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

Theorem oeeulem 8601
Description: Lemma for oeeu 8603. (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 4127 . . . . . . . 8 (𝐵 ∈ (On ∖ 1o) → 𝐵 ∈ On)
32adantl 483 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ On)
4 onsuc 7799 . . . . . . 7 (𝐵 ∈ On → suc 𝐵 ∈ On)
53, 4syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝐵 ∈ On)
6 oeworde 8593 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ suc 𝐵 ∈ On) → suc 𝐵 ⊆ (𝐴o suc 𝐵))
75, 6syldan 592 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝐵 ⊆ (𝐴o suc 𝐵))
8 sucidg 6446 . . . . . . . 8 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
93, 8syl 17 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ suc 𝐵)
107, 9sseldd 3984 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝐵))
11 oveq2 7417 . . . . . . . 8 (𝑥 = suc 𝐵 → (𝐴o 𝑥) = (𝐴o suc 𝐵))
1211eleq2d 2820 . . . . . . 7 (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o suc 𝐵)))
1312rspcev 3613 . . . . . 6 ((suc 𝐵 ∈ On ∧ 𝐵 ∈ (𝐴o suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
145, 10, 13syl2anc 585 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
15 onintrab2 7785 . . . . 5 (∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥) ↔ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
1614, 15sylib 217 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
17 onuni 7776 . . . 4 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
1816, 17syl 17 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
191, 18eqeltrid 2838 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ On)
20 sucidg 6446 . . . . . . 7 (𝑋 ∈ On → 𝑋 ∈ suc 𝑋)
2119, 20syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ suc 𝑋)
22 suceq 6431 . . . . . . . 8 (𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
231, 22ax-mp 5 . . . . . . 7 suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
24 dif1o 8500 . . . . . . . . . . . . 13 (𝐵 ∈ (On ∖ 1o) ↔ (𝐵 ∈ On ∧ 𝐵 ≠ ∅))
2524simprbi 498 . . . . . . . . . . . 12 (𝐵 ∈ (On ∖ 1o) → 𝐵 ≠ ∅)
2625adantl 483 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ≠ ∅)
27 ssrab2 4078 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ⊆ On
28 rabn0 4386 . . . . . . . . . . . . . . . 16 ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
2914, 28sylibr 233 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅)
30 onint 7778 . . . . . . . . . . . . . . 15 (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
3127, 29, 30sylancr 588 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
32 eleq1 2822 . . . . . . . . . . . . . 14 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
3331, 32syl5ibcom 244 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
34 oveq2 7417 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴o 𝑥) = (𝐴o ∅))
3534eleq2d 2820 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o ∅)))
3635elrab 3684 . . . . . . . . . . . . . . 15 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴o ∅)))
3736simprbi 498 . . . . . . . . . . . . . 14 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o ∅))
38 eldifi 4127 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
3938adantr 482 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐴 ∈ On)
40 oe0 8522 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → (𝐴o ∅) = 1o)
4139, 40syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o ∅) = 1o)
4241eleq2d 2820 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴o ∅) ↔ 𝐵 ∈ 1o))
43 el1o 8495 . . . . . . . . . . . . . . 15 (𝐵 ∈ 1o𝐵 = ∅)
4442, 43bitrdi 287 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴o ∅) ↔ 𝐵 = ∅))
4537, 44imbitrid 243 . . . . . . . . . . . . 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 6426 . . . . . . . . . . . . . . . . 17 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
5049, 1eqtr4di 2791 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋)
5150adantl 483 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋)
5231adantr 482 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
5351, 52eqeltrrd 2835 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
54 oveq2 7417 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → (𝐴o 𝑦) = (𝐴o 𝑋))
5554eleq2d 2820 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐵 ∈ (𝐴o 𝑦) ↔ 𝐵 ∈ (𝐴o 𝑋)))
56 oveq2 7417 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
5756eleq2d 2820 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o 𝑦)))
5857cbvrabv 3443 . . . . . . . . . . . . . . . 16 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)}
5955, 58elrab2 3687 . . . . . . . . . . . . . . 15 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴o 𝑋)))
6059simprbi 498 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o 𝑋))
6153, 60syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐵 ∈ (𝐴o 𝑋))
6238ad2antrr 725 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐴 ∈ On)
63 limeq 6377 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋 → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ Lim 𝑋))
6450, 63syl 17 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ Lim 𝑋))
6564ibi 267 . . . . . . . . . . . . . . 15 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → Lim 𝑋)
6619, 65anim12i 614 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝑋 ∈ On ∧ Lim 𝑋))
67 dif20el 8505 . . . . . . . . . . . . . . 15 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
6867ad2antrr 725 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ∅ ∈ 𝐴)
69 oelim 8534 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑋) = 𝑦𝑋 (𝐴o 𝑦))
7062, 66, 68, 69syl21anc 837 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝐴o 𝑋) = 𝑦𝑋 (𝐴o 𝑦))
7161, 70eleqtrd 2836 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐵 𝑦𝑋 (𝐴o 𝑦))
72 eliun 5002 . . . . . . . . . . . 12 (𝐵 𝑦𝑋 (𝐴o 𝑦) ↔ ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
7371, 72sylib 217 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
7419adantr 482 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ∈ On)
75 onss 7772 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → 𝑋 ⊆ On)
7674, 75syl 17 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ⊆ On)
7776sselda 3983 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → 𝑦 ∈ On)
7851eleq2d 2820 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ 𝑦𝑋))
7978biimpar 479 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → 𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
8057onnminsb 7787 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ¬ 𝐵 ∈ (𝐴o 𝑦)))
8177, 79, 80sylc 65 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → ¬ 𝐵 ∈ (𝐴o 𝑦))
8281nrexdv 3150 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ¬ ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
8373, 82pm2.65da 816 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
84 ioran 983 . . . . . . . . . 10 (¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ↔ (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∧ ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
8548, 83, 84sylanbrc 584 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
86 eloni 6375 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On → Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
87 unizlim 6488 . . . . . . . . . 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 325 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
90 orduniorsuc 7818 . . . . . . . . . 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 863 . . . . . . . 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 2792 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9521, 94eleqtrd 2836 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9658inteqi 4955 . . . . 5 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)}
9795, 96eleqtrdi 2844 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)})
9855onnminsb 7787 . . . 4 (𝑋 ∈ On → (𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)} → ¬ 𝐵 ∈ (𝐴o 𝑋)))
9919, 97, 98sylc 65 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ 𝐵 ∈ (𝐴o 𝑋))
100 oecl 8537 . . . . 5 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
10139, 19, 100syl2anc 585 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ∈ On)
102 ontri1 6399 . . . 4 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝑋)))
103101, 3, 102syl2anc 585 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐴o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝑋)))
10499, 103mpbird 257 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ⊆ 𝐵)
10594, 31eqeltrd 2834 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
106 oveq2 7417 . . . . . 6 (𝑦 = suc 𝑋 → (𝐴o 𝑦) = (𝐴o suc 𝑋))
107106eleq2d 2820 . . . . 5 (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴o 𝑦) ↔ 𝐵 ∈ (𝐴o suc 𝑋)))
108107, 58elrab2 3687 . . . 4 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴o suc 𝑋)))
109108simprbi 498 . . 3 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o suc 𝑋))
110105, 109syl 17 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝑋))
11119, 104, 1103jca 1129 1 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wrex 3071  {crab 3433  cdif 3946  wss 3949  c0 4323   cuni 4909   cint 4951   ciun 4998  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367  (class class class)co 7409  1oc1o 8459  2oc2o 8460  o coe 8465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-omul 8471  df-oexp 8472
This theorem is referenced by:  oeeui  8602  oeeu  8603
  Copyright terms: Public domain W3C validator