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

Theorem oeeulem 8338
Description: Lemma for oeeu 8340. (Contributed by Mario Carneiro, 28-Feb-2013.)
Hypothesis
Ref Expression
oeeu.1 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
Assertion
Ref Expression
oeeulem ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o 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 ∣ 𝐵 ∈ (𝐴o 𝑥)}
2 eldifi 4050 . . . . . . . 8 (𝐵 ∈ (On ∖ 1o) → 𝐵 ∈ On)
32adantl 485 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ On)
4 suceloni 7601 . . . . . . 7 (𝐵 ∈ On → suc 𝐵 ∈ On)
53, 4syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝐵 ∈ On)
6 oeworde 8330 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ suc 𝐵 ∈ On) → suc 𝐵 ⊆ (𝐴o suc 𝐵))
75, 6syldan 594 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝐵 ⊆ (𝐴o suc 𝐵))
8 sucidg 6300 . . . . . . . 8 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
93, 8syl 17 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ suc 𝐵)
107, 9sseldd 3911 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝐵))
11 oveq2 7230 . . . . . . . 8 (𝑥 = suc 𝐵 → (𝐴o 𝑥) = (𝐴o suc 𝐵))
1211eleq2d 2824 . . . . . . 7 (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o suc 𝐵)))
1312rspcev 3544 . . . . . 6 ((suc 𝐵 ∈ On ∧ 𝐵 ∈ (𝐴o suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
145, 10, 13syl2anc 587 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
15 onintrab2 7590 . . . . 5 (∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥) ↔ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
1614, 15sylib 221 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
17 onuni 7581 . . . 4 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
1816, 17syl 17 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
191, 18eqeltrid 2843 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ On)
20 sucidg 6300 . . . . . . 7 (𝑋 ∈ On → 𝑋 ∈ suc 𝑋)
2119, 20syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ suc 𝑋)
22 suceq 6287 . . . . . . . 8 (𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
231, 22ax-mp 5 . . . . . . 7 suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
24 dif1o 8236 . . . . . . . . . . . . 13 (𝐵 ∈ (On ∖ 1o) ↔ (𝐵 ∈ On ∧ 𝐵 ≠ ∅))
2524simprbi 500 . . . . . . . . . . . 12 (𝐵 ∈ (On ∖ 1o) → 𝐵 ≠ ∅)
2625adantl 485 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ≠ ∅)
27 ssrab2 4002 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ⊆ On
28 rabn0 4309 . . . . . . . . . . . . . . . 16 ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
2914, 28sylibr 237 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅)
30 onint 7583 . . . . . . . . . . . . . . 15 (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
3127, 29, 30sylancr 590 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
32 eleq1 2826 . . . . . . . . . . . . . 14 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
3331, 32syl5ibcom 248 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
34 oveq2 7230 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴o 𝑥) = (𝐴o ∅))
3534eleq2d 2824 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o ∅)))
3635elrab 3609 . . . . . . . . . . . . . . 15 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴o ∅)))
3736simprbi 500 . . . . . . . . . . . . . 14 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o ∅))
38 eldifi 4050 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
3938adantr 484 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐴 ∈ On)
40 oe0 8258 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → (𝐴o ∅) = 1o)
4139, 40syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o ∅) = 1o)
4241eleq2d 2824 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴o ∅) ↔ 𝐵 ∈ 1o))
43 el1o 8235 . . . . . . . . . . . . . . 15 (𝐵 ∈ 1o𝐵 = ∅)
4442, 43bitrdi 290 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴o ∅) ↔ 𝐵 = ∅))
4537, 44syl5ib 247 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 = ∅))
4633, 45syld 47 . . . . . . . . . . . 12 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → 𝐵 = ∅))
4746necon3ad 2954 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ≠ ∅ → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅))
4826, 47mpd 15 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅)
49 limuni 6282 . . . . . . . . . . . . . . . . 17 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
5049, 1eqtr4di 2797 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋)
5150adantl 485 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋)
5231adantr 484 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
5351, 52eqeltrrd 2840 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
54 oveq2 7230 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → (𝐴o 𝑦) = (𝐴o 𝑋))
5554eleq2d 2824 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐵 ∈ (𝐴o 𝑦) ↔ 𝐵 ∈ (𝐴o 𝑋)))
56 oveq2 7230 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
5756eleq2d 2824 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o 𝑦)))
5857cbvrabv 3409 . . . . . . . . . . . . . . . 16 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)}
5955, 58elrab2 3612 . . . . . . . . . . . . . . 15 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴o 𝑋)))
6059simprbi 500 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o 𝑋))
6153, 60syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐵 ∈ (𝐴o 𝑋))
6238ad2antrr 726 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐴 ∈ On)
63 limeq 6234 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋 → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ Lim 𝑋))
6450, 63syl 17 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ Lim 𝑋))
6564ibi 270 . . . . . . . . . . . . . . 15 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → Lim 𝑋)
6619, 65anim12i 616 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝑋 ∈ On ∧ Lim 𝑋))
67 dif20el 8241 . . . . . . . . . . . . . . 15 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
6867ad2antrr 726 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ∅ ∈ 𝐴)
69 oelim 8270 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑋) = 𝑦𝑋 (𝐴o 𝑦))
7062, 66, 68, 69syl21anc 838 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝐴o 𝑋) = 𝑦𝑋 (𝐴o 𝑦))
7161, 70eleqtrd 2841 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐵 𝑦𝑋 (𝐴o 𝑦))
72 eliun 4917 . . . . . . . . . . . 12 (𝐵 𝑦𝑋 (𝐴o 𝑦) ↔ ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
7371, 72sylib 221 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
7419adantr 484 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ∈ On)
75 onss 7577 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → 𝑋 ⊆ On)
7674, 75syl 17 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ⊆ On)
7776sselda 3910 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → 𝑦 ∈ On)
7851eleq2d 2824 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ 𝑦𝑋))
7978biimpar 481 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → 𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
8057onnminsb 7592 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ¬ 𝐵 ∈ (𝐴o 𝑦)))
8177, 79, 80sylc 65 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → ¬ 𝐵 ∈ (𝐴o 𝑦))
8281nrexdv 3196 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ¬ ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
8373, 82pm2.65da 817 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
84 ioran 984 . . . . . . . . . 10 (¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ↔ (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∧ ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
8548, 83, 84sylanbrc 586 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
86 eloni 6232 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On → Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
87 unizlim 6339 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})))
8816, 86, 873syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})))
8985, 88mtbird 328 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
90 orduniorsuc 7618 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
9116, 86, 903syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
9291ord 864 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
9389, 92mpd 15 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9423, 93eqtr4id 2798 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9521, 94eleqtrd 2841 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9658inteqi 4872 . . . . 5 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)}
9795, 96eleqtrdi 2849 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)})
9855onnminsb 7592 . . . 4 (𝑋 ∈ On → (𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)} → ¬ 𝐵 ∈ (𝐴o 𝑋)))
9919, 97, 98sylc 65 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ 𝐵 ∈ (𝐴o 𝑋))
100 oecl 8273 . . . . 5 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
10139, 19, 100syl2anc 587 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ∈ On)
102 ontri1 6256 . . . 4 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝑋)))
103101, 3, 102syl2anc 587 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐴o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝑋)))
10499, 103mpbird 260 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ⊆ 𝐵)
10594, 31eqeltrd 2839 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
106 oveq2 7230 . . . . . 6 (𝑦 = suc 𝑋 → (𝐴o 𝑦) = (𝐴o suc 𝑋))
107106eleq2d 2824 . . . . 5 (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴o 𝑦) ↔ 𝐵 ∈ (𝐴o suc 𝑋)))
108107, 58elrab2 3612 . . . 4 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴o suc 𝑋)))
109108simprbi 500 . . 3 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o suc 𝑋))
110105, 109syl 17 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝑋))
11119, 104, 1103jca 1130 1 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wcel 2111  wne 2941  wrex 3063  {crab 3066  cdif 3872  wss 3875  c0 4246   cuni 4828   cint 4868   ciun 4913  Ord word 6221  Oncon0 6222  Lim wlim 6223  suc csuc 6224  (class class class)co 7222  1oc1o 8204  2oc2o 8205  o coe 8210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5188  ax-sep 5201  ax-nul 5208  ax-pr 5331  ax-un 7532
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-pss 3894  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4829  df-int 4869  df-iun 4915  df-br 5063  df-opab 5125  df-mpt 5145  df-tr 5171  df-id 5464  df-eprel 5469  df-po 5477  df-so 5478  df-fr 5518  df-we 5520  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-pred 6169  df-ord 6225  df-on 6226  df-lim 6227  df-suc 6228  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-ov 7225  df-oprab 7226  df-mpo 7227  df-om 7654  df-wrecs 8056  df-recs 8117  df-rdg 8155  df-1o 8211  df-2o 8212  df-oadd 8215  df-omul 8216  df-oexp 8217
This theorem is referenced by:  oeeui  8339  oeeu  8340
  Copyright terms: Public domain W3C validator