MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oeeulem Structured version   Visualization version   GIF version

Theorem oeeulem 7726
Description: Lemma for oeeu 7728. (Contributed by Mario Carneiro, 28-Feb-2013.)
Hypothesis
Ref Expression
oeeu.1 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
Assertion
Ref Expression
oeeulem ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝑋 ∈ On ∧ (𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝑋(𝑥)

Proof of Theorem oeeulem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 oeeu.1 . . 3 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
2 eldifi 3765 . . . . . . . 8 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ∈ On)
32adantl 481 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ On)
4 suceloni 7055 . . . . . . 7 (𝐵 ∈ On → suc 𝐵 ∈ On)
53, 4syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝐵 ∈ On)
6 oeworde 7718 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2𝑜) ∧ suc 𝐵 ∈ On) → suc 𝐵 ⊆ (𝐴𝑜 suc 𝐵))
75, 6syldan 486 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝐵 ⊆ (𝐴𝑜 suc 𝐵))
8 sucidg 5841 . . . . . . . 8 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
93, 8syl 17 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ suc 𝐵)
107, 9sseldd 3637 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝐵))
11 oveq2 6698 . . . . . . . 8 (𝑥 = suc 𝐵 → (𝐴𝑜 𝑥) = (𝐴𝑜 suc 𝐵))
1211eleq2d 2716 . . . . . . 7 (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴𝑜 𝑥) ↔ 𝐵 ∈ (𝐴𝑜 suc 𝐵)))
1312rspcev 3340 . . . . . 6 ((suc 𝐵 ∈ On ∧ 𝐵 ∈ (𝐴𝑜 suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥))
145, 10, 13syl2anc 694 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥))
15 onintrab2 7044 . . . . 5 (∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥) ↔ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
1614, 15sylib 208 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
17 onuni 7035 . . . 4 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
1816, 17syl 17 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
191, 18syl5eqel 2734 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ On)
20 sucidg 5841 . . . . . . 7 (𝑋 ∈ On → 𝑋 ∈ suc 𝑋)
2119, 20syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ suc 𝑋)
22 dif1o 7625 . . . . . . . . . . . . 13 (𝐵 ∈ (On ∖ 1𝑜) ↔ (𝐵 ∈ On ∧ 𝐵 ≠ ∅))
2322simprbi 479 . . . . . . . . . . . 12 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ≠ ∅)
2423adantl 481 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ≠ ∅)
25 ssrab2 3720 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ⊆ On
26 rabn0 3991 . . . . . . . . . . . . . . . 16 ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥))
2714, 26sylibr 224 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ≠ ∅)
28 onint 7037 . . . . . . . . . . . . . . 15 (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ≠ ∅) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
2925, 27, 28sylancr 696 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
30 eleq1 2718 . . . . . . . . . . . . . 14 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
3129, 30syl5ibcom 235 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
32 oveq2 6698 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴𝑜 𝑥) = (𝐴𝑜 ∅))
3332eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴𝑜 𝑥) ↔ 𝐵 ∈ (𝐴𝑜 ∅)))
3433elrab 3396 . . . . . . . . . . . . . . 15 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴𝑜 ∅)))
3534simprbi 479 . . . . . . . . . . . . . 14 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 ∈ (𝐴𝑜 ∅))
36 eldifi 3765 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → 𝐴 ∈ On)
3736adantr 480 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐴 ∈ On)
38 oe0 7647 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → (𝐴𝑜 ∅) = 1𝑜)
3937, 38syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 ∅) = 1𝑜)
4039eleq2d 2716 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐵 ∈ (𝐴𝑜 ∅) ↔ 𝐵 ∈ 1𝑜))
41 el1o 7624 . . . . . . . . . . . . . . 15 (𝐵 ∈ 1𝑜𝐵 = ∅)
4240, 41syl6bb 276 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐵 ∈ (𝐴𝑜 ∅) ↔ 𝐵 = ∅))
4335, 42syl5ib 234 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 = ∅))
4431, 43syld 47 . . . . . . . . . . . 12 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ → 𝐵 = ∅))
4544necon3ad 2836 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐵 ≠ ∅ → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅))
4624, 45mpd 15 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅)
47 limuni 5823 . . . . . . . . . . . . . . . . 17 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
4847, 1syl6eqr 2703 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = 𝑋)
4948adantl 481 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = 𝑋)
5029adantr 480 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
5149, 50eqeltrrd 2731 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
52 oveq2 6698 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → (𝐴𝑜 𝑦) = (𝐴𝑜 𝑋))
5352eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐵 ∈ (𝐴𝑜 𝑦) ↔ 𝐵 ∈ (𝐴𝑜 𝑋)))
54 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 𝑦))
5554eleq2d 2716 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐵 ∈ (𝐴𝑜 𝑥) ↔ 𝐵 ∈ (𝐴𝑜 𝑦)))
5655cbvrabv 3230 . . . . . . . . . . . . . . . 16 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)}
5753, 56elrab2 3399 . . . . . . . . . . . . . . 15 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴𝑜 𝑋)))
5857simprbi 479 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 ∈ (𝐴𝑜 𝑋))
5951, 58syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝐵 ∈ (𝐴𝑜 𝑋))
6036ad2antrr 762 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝐴 ∈ On)
61 limeq 5773 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = 𝑋 → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ Lim 𝑋))
6248, 61syl 17 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ Lim 𝑋))
6362ibi 256 . . . . . . . . . . . . . . 15 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → Lim 𝑋)
6419, 63anim12i 589 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → (𝑋 ∈ On ∧ Lim 𝑋))
65 dif20el 7630 . . . . . . . . . . . . . . 15 (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴)
6665ad2antrr 762 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → ∅ ∈ 𝐴)
67 oelim 7659 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝑋) = 𝑦𝑋 (𝐴𝑜 𝑦))
6860, 64, 66, 67syl21anc 1365 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → (𝐴𝑜 𝑋) = 𝑦𝑋 (𝐴𝑜 𝑦))
6959, 68eleqtrd 2732 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝐵 𝑦𝑋 (𝐴𝑜 𝑦))
70 eliun 4556 . . . . . . . . . . . 12 (𝐵 𝑦𝑋 (𝐴𝑜 𝑦) ↔ ∃𝑦𝑋 𝐵 ∈ (𝐴𝑜 𝑦))
7169, 70sylib 208 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → ∃𝑦𝑋 𝐵 ∈ (𝐴𝑜 𝑦))
7219adantr 480 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝑋 ∈ On)
73 onss 7032 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → 𝑋 ⊆ On)
7472, 73syl 17 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝑋 ⊆ On)
7574sselda 3636 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ∧ 𝑦𝑋) → 𝑦 ∈ On)
7649eleq2d 2716 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ 𝑦𝑋))
7776biimpar 501 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ∧ 𝑦𝑋) → 𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
7855onnminsb 7046 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → ¬ 𝐵 ∈ (𝐴𝑜 𝑦)))
7975, 77, 78sylc 65 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ∧ 𝑦𝑋) → ¬ 𝐵 ∈ (𝐴𝑜 𝑦))
8079nrexdv 3030 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → ¬ ∃𝑦𝑋 𝐵 ∈ (𝐴𝑜 𝑦))
8171, 80pm2.65da 599 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
82 ioran 510 . . . . . . . . . 10 (¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ↔ (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∧ ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
8346, 81, 82sylanbrc 699 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
84 eloni 5771 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On → Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
85 unizlim 5882 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})))
8616, 84, 853syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})))
8783, 86mtbird 314 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
88 orduniorsuc 7072 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
8916, 84, 883syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
9089ord 391 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
9187, 90mpd 15 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
92 suceq 5828 . . . . . . . 8 (𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
931, 92ax-mp 5 . . . . . . 7 suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
9491, 93syl6reqr 2704 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
9521, 94eleqtrd 2732 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
9656inteqi 4511 . . . . 5 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)}
9795, 96syl6eleq 2740 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)})
9853onnminsb 7046 . . . 4 (𝑋 ∈ On → (𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)} → ¬ 𝐵 ∈ (𝐴𝑜 𝑋)))
9919, 97, 98sylc 65 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ 𝐵 ∈ (𝐴𝑜 𝑋))
100 oecl 7662 . . . . 5 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴𝑜 𝑋) ∈ On)
10137, 19, 100syl2anc 694 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ∈ On)
102 ontri1 5795 . . . 4 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴𝑜 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝑋)))
103101, 3, 102syl2anc 694 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐴𝑜 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝑋)))
10499, 103mpbird 247 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
10594, 29eqeltrd 2730 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
106 oveq2 6698 . . . . . 6 (𝑦 = suc 𝑋 → (𝐴𝑜 𝑦) = (𝐴𝑜 suc 𝑋))
107106eleq2d 2716 . . . . 5 (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴𝑜 𝑦) ↔ 𝐵 ∈ (𝐴𝑜 suc 𝑋)))
108107, 56elrab2 3399 . . . 4 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴𝑜 suc 𝑋)))
109108simprbi 479 . . 3 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
110105, 109syl 17 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
11119, 104, 1103jca 1261 1 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝑋 ∈ On ∧ (𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wrex 2942  {crab 2945  cdif 3604  wss 3607  c0 3948   cuni 4468   cint 4507   ciun 4552  Ord word 5760  Oncon0 5761  Lim wlim 5762  suc csuc 5763  (class class class)co 6690  1𝑜c1o 7598  2𝑜c2o 7599  𝑜 coe 7604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-oexp 7611
This theorem is referenced by:  oeeui  7727  oeeu  7728
  Copyright terms: Public domain W3C validator