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

Theorem oeeulem 7633
 Description: Lemma for oeeu 7635. (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 3715 . . . . . . . 8 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ∈ On)
32adantl 482 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ On)
4 suceloni 6967 . . . . . . 7 (𝐵 ∈ On → suc 𝐵 ∈ On)
53, 4syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝐵 ∈ On)
6 oeworde 7625 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2𝑜) ∧ suc 𝐵 ∈ On) → suc 𝐵 ⊆ (𝐴𝑜 suc 𝐵))
75, 6syldan 487 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝐵 ⊆ (𝐴𝑜 suc 𝐵))
8 sucidg 5767 . . . . . . . 8 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
93, 8syl 17 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ suc 𝐵)
107, 9sseldd 3588 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝐵))
11 oveq2 6618 . . . . . . . 8 (𝑥 = suc 𝐵 → (𝐴𝑜 𝑥) = (𝐴𝑜 suc 𝐵))
1211eleq2d 2684 . . . . . . 7 (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴𝑜 𝑥) ↔ 𝐵 ∈ (𝐴𝑜 suc 𝐵)))
1312rspcev 3298 . . . . . 6 ((suc 𝐵 ∈ On ∧ 𝐵 ∈ (𝐴𝑜 suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥))
145, 10, 13syl2anc 692 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥))
15 onintrab2 6956 . . . . 5 (∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥) ↔ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
1614, 15sylib 208 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
17 onuni 6947 . . . 4 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
1816, 17syl 17 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On)
191, 18syl5eqel 2702 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ On)
20 sucidg 5767 . . . . . . 7 (𝑋 ∈ On → 𝑋 ∈ suc 𝑋)
2119, 20syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ suc 𝑋)
22 dif1o 7532 . . . . . . . . . . . . 13 (𝐵 ∈ (On ∖ 1𝑜) ↔ (𝐵 ∈ On ∧ 𝐵 ≠ ∅))
2322simprbi 480 . . . . . . . . . . . 12 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ≠ ∅)
2423adantl 482 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ≠ ∅)
25 ssrab2 3671 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ⊆ On
26 rabn0 3937 . . . . . . . . . . . . . . . 16 ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴𝑜 𝑥))
2714, 26sylibr 224 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ≠ ∅)
28 onint 6949 . . . . . . . . . . . . . . 15 (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ≠ ∅) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
2925, 27, 28sylancr 694 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
30 eleq1 2686 . . . . . . . . . . . . . 14 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
3129, 30syl5ibcom 235 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
32 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴𝑜 𝑥) = (𝐴𝑜 ∅))
3332eleq2d 2684 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴𝑜 𝑥) ↔ 𝐵 ∈ (𝐴𝑜 ∅)))
3433elrab 3350 . . . . . . . . . . . . . . 15 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴𝑜 ∅)))
3534simprbi 480 . . . . . . . . . . . . . 14 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 ∈ (𝐴𝑜 ∅))
36 eldifi 3715 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → 𝐴 ∈ On)
3736adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐴 ∈ On)
38 oe0 7554 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → (𝐴𝑜 ∅) = 1𝑜)
3937, 38syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 ∅) = 1𝑜)
4039eleq2d 2684 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐵 ∈ (𝐴𝑜 ∅) ↔ 𝐵 ∈ 1𝑜))
41 el1o 7531 . . . . . . . . . . . . . . 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 2803 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐵 ≠ ∅ → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅))
4624, 45mpd 15 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅)
47 limuni 5749 . . . . . . . . . . . . . . . . 17 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
4847, 1syl6eqr 2673 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = 𝑋)
4948adantl 482 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = 𝑋)
5029adantr 481 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
5149, 50eqeltrrd 2699 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
52 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → (𝐴𝑜 𝑦) = (𝐴𝑜 𝑋))
5352eleq2d 2684 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐵 ∈ (𝐴𝑜 𝑦) ↔ 𝐵 ∈ (𝐴𝑜 𝑋)))
54 oveq2 6618 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 𝑦))
5554eleq2d 2684 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐵 ∈ (𝐴𝑜 𝑥) ↔ 𝐵 ∈ (𝐴𝑜 𝑦)))
5655cbvrabv 3188 . . . . . . . . . . . . . . . 16 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)}
5753, 56elrab2 3352 . . . . . . . . . . . . . . 15 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴𝑜 𝑋)))
5857simprbi 480 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 ∈ (𝐴𝑜 𝑋))
5951, 58syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝐵 ∈ (𝐴𝑜 𝑋))
6036ad2antrr 761 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝐴 ∈ On)
61 limeq 5699 . . . . . . . . . . . . . . . . 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 7537 . . . . . . . . . . . . . . 15 (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴)
6665ad2antrr 761 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → ∅ ∈ 𝐴)
67 oelim 7566 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝑋) = 𝑦𝑋 (𝐴𝑜 𝑦))
6860, 64, 66, 67syl21anc 1322 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → (𝐴𝑜 𝑋) = 𝑦𝑋 (𝐴𝑜 𝑦))
6959, 68eleqtrd 2700 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝐵 𝑦𝑋 (𝐴𝑜 𝑦))
70 eliun 4495 . . . . . . . . . . . 12 (𝐵 𝑦𝑋 (𝐴𝑜 𝑦) ↔ ∃𝑦𝑋 𝐵 ∈ (𝐴𝑜 𝑦))
7169, 70sylib 208 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → ∃𝑦𝑋 𝐵 ∈ (𝐴𝑜 𝑦))
7219adantr 481 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝑋 ∈ On)
73 onss 6944 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → 𝑋 ⊆ On)
7472, 73syl 17 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → 𝑋 ⊆ On)
7574sselda 3587 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ∧ 𝑦𝑋) → 𝑦 ∈ On)
7649eleq2d 2684 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ 𝑦𝑋))
7776biimpar 502 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ∧ 𝑦𝑋) → 𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
7855onnminsb 6958 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → ¬ 𝐵 ∈ (𝐴𝑜 𝑦)))
7975, 77, 78sylc 65 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ∧ 𝑦𝑋) → ¬ 𝐵 ∈ (𝐴𝑜 𝑦))
8079nrexdv 2996 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) → ¬ ∃𝑦𝑋 𝐵 ∈ (𝐴𝑜 𝑦))
8171, 80pm2.65da 599 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
82 ioran 511 . . . . . . . . . 10 (¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}) ↔ (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∧ ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
8346, 81, 82sylanbrc 697 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
84 eloni 5697 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∈ On → Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
85 unizlim 5808 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})))
8616, 84, 853syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})))
8783, 86mtbird 315 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
88 orduniorsuc 6984 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
8916, 84, 883syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
9089ord 392 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}))
9187, 90mpd 15 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
92 suceq 5754 . . . . . . . 8 (𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
931, 92ax-mp 5 . . . . . . 7 suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
9491, 93syl6reqr 2674 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
9521, 94eleqtrd 2700 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
9656inteqi 4449 . . . . 5 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)}
9795, 96syl6eleq 2708 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)})
9853onnminsb 6958 . . . 4 (𝑋 ∈ On → (𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑦)} → ¬ 𝐵 ∈ (𝐴𝑜 𝑋)))
9919, 97, 98sylc 65 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ¬ 𝐵 ∈ (𝐴𝑜 𝑋))
100 oecl 7569 . . . . 5 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴𝑜 𝑋) ∈ On)
10137, 19, 100syl2anc 692 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ∈ On)
102 ontri1 5721 . . . 4 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴𝑜 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝑋)))
103101, 3, 102syl2anc 692 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐴𝑜 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝑋)))
10499, 103mpbird 247 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
10594, 29eqeltrd 2698 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)})
106 oveq2 6618 . . . . . 6 (𝑦 = suc 𝑋 → (𝐴𝑜 𝑦) = (𝐴𝑜 suc 𝑋))
107106eleq2d 2684 . . . . 5 (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴𝑜 𝑦) ↔ 𝐵 ∈ (𝐴𝑜 suc 𝑋)))
108107, 56elrab2 3352 . . . 4 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴𝑜 suc 𝑋)))
109108simprbi 480 . . 3 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)} → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
110105, 109syl 17 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
11119, 104, 1103jca 1240 1 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝑋 ∈ On ∧ (𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908  {crab 2911   ∖ cdif 3556   ⊆ wss 3559  ∅c0 3896  ∪ cuni 4407  ∩ cint 4445  ∪ ciun 4490  Ord word 5686  Oncon0 5687  Lim wlim 5688  suc csuc 5689  (class class class)co 6610  1𝑜c1o 7505  2𝑜c2o 7506   ↑𝑜 coe 7511 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-omul 7517  df-oexp 7518 This theorem is referenced by:  oeeui  7634  oeeu  7635
 Copyright terms: Public domain W3C validator