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

Theorem oeeulem 8205
Description: Lemma for oeeu 8207. (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 4082 . . . . . . . 8 (𝐵 ∈ (On ∖ 1o) → 𝐵 ∈ On)
32adantl 484 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ On)
4 suceloni 7506 . . . . . . 7 (𝐵 ∈ On → suc 𝐵 ∈ On)
53, 4syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝐵 ∈ On)
6 oeworde 8197 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ suc 𝐵 ∈ On) → suc 𝐵 ⊆ (𝐴o suc 𝐵))
75, 6syldan 593 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝐵 ⊆ (𝐴o suc 𝐵))
8 sucidg 6245 . . . . . . . 8 (𝐵 ∈ On → 𝐵 ∈ suc 𝐵)
93, 8syl 17 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ suc 𝐵)
107, 9sseldd 3947 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝐵))
11 oveq2 7141 . . . . . . . 8 (𝑥 = suc 𝐵 → (𝐴o 𝑥) = (𝐴o suc 𝐵))
1211eleq2d 2896 . . . . . . 7 (𝑥 = suc 𝐵 → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o suc 𝐵)))
1312rspcev 3602 . . . . . 6 ((suc 𝐵 ∈ On ∧ 𝐵 ∈ (𝐴o suc 𝐵)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
145, 10, 13syl2anc 586 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
15 onintrab2 7495 . . . . 5 (∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥) ↔ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
1614, 15sylib 220 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
17 onuni 7486 . . . 4 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
1816, 17syl 17 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On)
191, 18eqeltrid 2915 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ On)
20 sucidg 6245 . . . . . . 7 (𝑋 ∈ On → 𝑋 ∈ suc 𝑋)
2119, 20syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ suc 𝑋)
22 dif1o 8103 . . . . . . . . . . . . 13 (𝐵 ∈ (On ∖ 1o) ↔ (𝐵 ∈ On ∧ 𝐵 ≠ ∅))
2322simprbi 499 . . . . . . . . . . . 12 (𝐵 ∈ (On ∖ 1o) → 𝐵 ≠ ∅)
2423adantl 484 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ≠ ∅)
25 ssrab2 4035 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ⊆ On
26 rabn0 4315 . . . . . . . . . . . . . . . 16 ({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐵 ∈ (𝐴o 𝑥))
2714, 26sylibr 236 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅)
28 onint 7488 . . . . . . . . . . . . . . 15 (({𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ⊆ On ∧ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ≠ ∅) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
2925, 27, 28sylancr 589 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
30 eleq1 2898 . . . . . . . . . . . . . 14 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
3129, 30syl5ibcom 247 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → ∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
32 oveq2 7141 . . . . . . . . . . . . . . . . 17 (𝑥 = ∅ → (𝐴o 𝑥) = (𝐴o ∅))
3332eleq2d 2896 . . . . . . . . . . . . . . . 16 (𝑥 = ∅ → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o ∅)))
3433elrab 3660 . . . . . . . . . . . . . . 15 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (∅ ∈ On ∧ 𝐵 ∈ (𝐴o ∅)))
3534simprbi 499 . . . . . . . . . . . . . 14 (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o ∅))
36 eldifi 4082 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
3736adantr 483 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐴 ∈ On)
38 oe0 8125 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → (𝐴o ∅) = 1o)
3937, 38syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o ∅) = 1o)
4039eleq2d 2896 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴o ∅) ↔ 𝐵 ∈ 1o))
41 el1o 8102 . . . . . . . . . . . . . . 15 (𝐵 ∈ 1o𝐵 = ∅)
4240, 41syl6bb 289 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ∈ (𝐴o ∅) ↔ 𝐵 = ∅))
4335, 42syl5ib 246 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (∅ ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 = ∅))
4431, 43syld 47 . . . . . . . . . . . 12 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ → 𝐵 = ∅))
4544necon3ad 3019 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐵 ≠ ∅ → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅))
4624, 45mpd 15 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅)
47 limuni 6227 . . . . . . . . . . . . . . . . 17 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
4847, 1syl6eqr 2873 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋)
4948adantl 484 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋)
5029adantr 483 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
5149, 50eqeltrrd 2912 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
52 oveq2 7141 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → (𝐴o 𝑦) = (𝐴o 𝑋))
5352eleq2d 2896 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐵 ∈ (𝐴o 𝑦) ↔ 𝐵 ∈ (𝐴o 𝑋)))
54 oveq2 7141 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
5554eleq2d 2896 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐵 ∈ (𝐴o 𝑥) ↔ 𝐵 ∈ (𝐴o 𝑦)))
5655cbvrabv 3470 . . . . . . . . . . . . . . . 16 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)}
5753, 56elrab2 3663 . . . . . . . . . . . . . . 15 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (𝑋 ∈ On ∧ 𝐵 ∈ (𝐴o 𝑋)))
5857simprbi 499 . . . . . . . . . . . . . 14 (𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o 𝑋))
5951, 58syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐵 ∈ (𝐴o 𝑋))
6036ad2antrr 724 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐴 ∈ On)
61 limeq 6179 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = 𝑋 → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ Lim 𝑋))
6248, 61syl 17 . . . . . . . . . . . . . . . 16 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ Lim 𝑋))
6362ibi 269 . . . . . . . . . . . . . . 15 (Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → Lim 𝑋)
6419, 63anim12i 614 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝑋 ∈ On ∧ Lim 𝑋))
65 dif20el 8108 . . . . . . . . . . . . . . 15 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
6665ad2antrr 724 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ∅ ∈ 𝐴)
67 oelim 8137 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ (𝑋 ∈ On ∧ Lim 𝑋)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑋) = 𝑦𝑋 (𝐴o 𝑦))
6860, 64, 66, 67syl21anc 835 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝐴o 𝑋) = 𝑦𝑋 (𝐴o 𝑦))
6959, 68eleqtrd 2913 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝐵 𝑦𝑋 (𝐴o 𝑦))
70 eliun 4899 . . . . . . . . . . . 12 (𝐵 𝑦𝑋 (𝐴o 𝑦) ↔ ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
7169, 70sylib 220 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
7219adantr 483 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ∈ On)
73 onss 7483 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → 𝑋 ⊆ On)
7472, 73syl 17 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → 𝑋 ⊆ On)
7574sselda 3946 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → 𝑦 ∈ On)
7649eleq2d 2896 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ 𝑦𝑋))
7776biimpar 480 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → 𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
7855onnminsb 7497 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ¬ 𝐵 ∈ (𝐴o 𝑦)))
7975, 77, 78sylc 65 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ∧ 𝑦𝑋) → ¬ 𝐵 ∈ (𝐴o 𝑦))
8079nrexdv 3257 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) → ¬ ∃𝑦𝑋 𝐵 ∈ (𝐴o 𝑦))
8171, 80pm2.65da 815 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
82 ioran 980 . . . . . . . . . 10 (¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}) ↔ (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∧ ¬ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
8346, 81, 82sylanbrc 585 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
84 eloni 6177 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∈ On → Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
85 unizlim 6283 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})))
8616, 84, 853syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = ∅ ∨ Lim {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})))
8783, 86mtbird 327 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
88 orduniorsuc 7523 . . . . . . . . . 10 (Ord {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
8916, 84, 883syl 18 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ( {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ∨ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
9089ord 860 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (¬ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}))
9187, 90mpd 15 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
92 suceq 6232 . . . . . . . 8 (𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
931, 92ax-mp 5 . . . . . . 7 suc 𝑋 = suc {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
9491, 93syl6reqr 2874 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9521, 94eleqtrd 2913 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
9656inteqi 4856 . . . . 5 {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} = {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)}
9795, 96eleqtrdi 2921 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)})
9853onnminsb 7497 . . . 4 (𝑋 ∈ On → (𝑋 {𝑦 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑦)} → ¬ 𝐵 ∈ (𝐴o 𝑋)))
9919, 97, 98sylc 65 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ¬ 𝐵 ∈ (𝐴o 𝑋))
100 oecl 8140 . . . . 5 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
10137, 19, 100syl2anc 586 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ∈ On)
102 ontri1 6201 . . . 4 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On) → ((𝐴o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝑋)))
103101, 3, 102syl2anc 586 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐴o 𝑋) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝑋)))
10499, 103mpbird 259 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ⊆ 𝐵)
10594, 29eqeltrd 2911 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)})
106 oveq2 7141 . . . . . 6 (𝑦 = suc 𝑋 → (𝐴o 𝑦) = (𝐴o suc 𝑋))
107106eleq2d 2896 . . . . 5 (𝑦 = suc 𝑋 → (𝐵 ∈ (𝐴o 𝑦) ↔ 𝐵 ∈ (𝐴o suc 𝑋)))
108107, 56elrab2 3663 . . . 4 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} ↔ (suc 𝑋 ∈ On ∧ 𝐵 ∈ (𝐴o suc 𝑋)))
109108simprbi 499 . . 3 (suc 𝑋 ∈ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)} → 𝐵 ∈ (𝐴o suc 𝑋))
110105, 109syl 17 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝑋))
11119, 104, 1103jca 1124 1 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1083   = wceq 1537  wcel 2114  wne 3006  wrex 3126  {crab 3129  cdif 3910  wss 3913  c0 4269   cuni 4814   cint 4852   ciun 4895  Ord word 6166  Oncon0 6167  Lim wlim 6168  suc csuc 6169  (class class class)co 7133  1oc1o 8073  2oc2o 8074  o coe 8079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-2o 8081  df-oadd 8084  df-omul 8085  df-oexp 8086
This theorem is referenced by:  oeeui  8206  oeeu  8207
  Copyright terms: Public domain W3C validator