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

Theorem domtriomlem 9552
Description: Lemma for domtriom 9553. (Contributed by Mario Carneiro, 9-Feb-2013.)
Hypotheses
Ref Expression
domtriomlem.1 𝐴 ∈ V
domtriomlem.2 𝐵 = {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)}
domtriomlem.3 𝐶 = (𝑛 ∈ ω ↦ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
Assertion
Ref Expression
domtriomlem 𝐴 ∈ Fin → ω ≼ 𝐴)
Distinct variable groups:   𝐴,𝑏,𝑛,𝑦   𝐵,𝑏   𝐶,𝑘,𝑛   𝑘,𝑏   𝑦,𝑏
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑦,𝑘,𝑛)   𝐶(𝑦,𝑏)

Proof of Theorem domtriomlem
Dummy variables 𝑐 𝑚 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 domtriomlem.2 . . . . 5 𝐵 = {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)}
2 domtriomlem.1 . . . . . . 7 𝐴 ∈ V
32pwex 5057 . . . . . 6 𝒫 𝐴 ∈ V
4 simpl 470 . . . . . . . 8 ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) → 𝑦𝐴)
54ss2abi 3878 . . . . . . 7 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦𝑦𝐴}
6 df-pw 4360 . . . . . . 7 𝒫 𝐴 = {𝑦𝑦𝐴}
75, 6sseqtr4i 3842 . . . . . 6 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
83, 7ssexi 5005 . . . . 5 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ∈ V
91, 8eqeltri 2888 . . . 4 𝐵 ∈ V
10 omex 8790 . . . . 5 ω ∈ V
1110enref 8228 . . . 4 ω ≈ ω
129, 11axcc3 9548 . . 3 𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
13 nfv 2005 . . . . . . . 8 𝑛 ¬ 𝐴 ∈ Fin
14 nfra1 3136 . . . . . . . 8 𝑛𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)
1513, 14nfan 1990 . . . . . . 7 𝑛𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
16 nnfi 8395 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → 𝑛 ∈ Fin)
17 pwfi 8503 . . . . . . . . . . . . . 14 (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
1816, 17sylib 209 . . . . . . . . . . . . 13 (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19 ficardom 9073 . . . . . . . . . . . . 13 (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20 isinf 8415 . . . . . . . . . . . . . 14 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚))
21 breq2 4855 . . . . . . . . . . . . . . . . 17 (𝑚 = (card‘𝒫 𝑛) → (𝑦𝑚𝑦 ≈ (card‘𝒫 𝑛)))
2221anbi2d 616 . . . . . . . . . . . . . . . 16 (𝑚 = (card‘𝒫 𝑛) → ((𝑦𝐴𝑦𝑚) ↔ (𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2322exbidv 2012 . . . . . . . . . . . . . . 15 (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦𝐴𝑦𝑚) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2423rspcv 3505 . . . . . . . . . . . . . 14 ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2520, 24syl5 34 . . . . . . . . . . . . 13 ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2618, 19, 253syl 18 . . . . . . . . . . . 12 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
27 finnum 9060 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28 cardid2 9065 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29 entr 8247 . . . . . . . . . . . . . . . 16 ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
3029expcom 400 . . . . . . . . . . . . . . 15 ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3231anim2d 601 . . . . . . . . . . . . 13 (𝑛 ∈ ω → ((𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3332eximdv 2008 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3426, 33syld 47 . . . . . . . . . . 11 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
351neeq1i 3049 . . . . . . . . . . . 12 (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36 abn0 4162 . . . . . . . . . . . 12 ({𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3735, 36bitri 266 . . . . . . . . . . 11 (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3834, 37syl6ibr 243 . . . . . . . . . 10 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
3938com12 32 . . . . . . . . 9 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
4039adantr 468 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41 rsp 3124 . . . . . . . . 9 (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4241adantl 469 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4340, 42mpdd 43 . . . . . . 7 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
4415, 43ralrimi 3152 . . . . . 6 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
45443adant2 1154 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
46453expib 1145 . . . 4 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4746eximdv 2008 . . 3 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4812, 47mpi 20 . 2 𝐴 ∈ Fin → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
49 axcc2 9547 . . . . 5 𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
50 simp2 1160 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → 𝑐 Fn ω)
51 nfra1 3136 . . . . . . . . . . 11 𝑛𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵
52 nfra1 3136 . . . . . . . . . . 11 𝑛𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))
5351, 52nfan 1990 . . . . . . . . . 10 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
54 fvex 6424 . . . . . . . . . . . . . . . 16 (𝑏𝑛) ∈ V
55 sseq1 3830 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦𝐴 ↔ (𝑏𝑛) ⊆ 𝐴))
56 breq1 4854 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏𝑛) ≈ 𝒫 𝑛))
5755, 56anbi12d 618 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏𝑛) → ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛)))
5854, 57, 1elab2 3556 . . . . . . . . . . . . . . 15 ((𝑏𝑛) ∈ 𝐵 ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛))
5958simprbi 486 . . . . . . . . . . . . . 14 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ≈ 𝒫 𝑛)
6059ralimi 3147 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛)
61 fveq2 6411 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑏𝑛) = (𝑏𝑘))
62 pweq 4361 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
6361, 62breq12d 4864 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ((𝑏𝑛) ≈ 𝒫 𝑛 ↔ (𝑏𝑘) ≈ 𝒫 𝑘))
6463cbvralv 3367 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘)
65 peano2 7319 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66 omelon 8793 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
6766onelssi 6052 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68 ssralv 3870 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
6965, 67, 683syl 18 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
70 pwsdompw 9314 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘) → 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛))
7170ex 399 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
7269, 71syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
73 sdomdif 8350 . . . . . . . . . . . . . . . 16 ( 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛) → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅)
7472, 73syl6 35 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7564, 74syl5bi 233 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
76 difss 3943 . . . . . . . . . . . . . . . . 17 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ⊆ (𝑏𝑛)
7754, 76ssexi 5005 . . . . . . . . . . . . . . . 16 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V
78 domtriomlem.3 . . . . . . . . . . . . . . . . 17 𝐶 = (𝑛 ∈ ω ↦ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7978fvmpt2 6515 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V) → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8077, 79mpan2 674 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8180neeq1d 3044 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ ↔ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
8275, 81sylibrd 250 . . . . . . . . . . . . 13 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → (𝐶𝑛) ≠ ∅))
8360, 82syl5com 31 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
8483adantr 468 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
85 rsp 3124 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8685adantl 469 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8784, 86mpdd 43 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
8853, 87ralrimi 3152 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
89883adant2 1154 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
9050, 89jca 503 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
91903expib 1145 . . . . . 6 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9291eximdv 2008 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9349, 92mpi 20 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
94 simp2 1160 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐 Fn ω)
95 nfra1 3136 . . . . . . . . . . . . 13 𝑛𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)
9651, 95nfan 1990 . . . . . . . . . . . 12 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
97 rsp 3124 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
9897com12 32 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝐶𝑛)))
99 rsp 3124 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
10099com12 32 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ∈ 𝐵))
10180eleq2d 2878 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) ↔ (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
102 eldifi 3938 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ (𝑏𝑛))
103101, 102syl6bi 244 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑛)))
10458simplbi 487 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ⊆ 𝐴)
105104sseld 3804 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝐴))
106103, 105syl9 77 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
107100, 106syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
108107com23 86 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
10998, 108syld 47 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
110109com13 88 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴)))
111110imp 395 . . . . . . . . . . . 12 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴))
11296, 111ralrimi 3152 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
1131123adant2 1154 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
114 ffnfv 6613 . . . . . . . . . 10 (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴))
11594, 113, 114sylanbrc 574 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω⟶𝐴)
116 nfv 2005 . . . . . . . . . . . 12 𝑛 𝑘 ∈ ω
117 nnord 7306 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
118 nnord 7306 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → Ord 𝑛)
119 ordtri3or 5975 . . . . . . . . . . . . . . . 16 ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
120117, 118, 119syl2an 585 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
121 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (𝑐𝑛) = (𝑐𝑘))
122 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑗 → (𝑏𝑘) = (𝑏𝑗))
123122cbviunv 4758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑘𝑛 (𝑏𝑘) = 𝑗𝑛 (𝑏𝑗)
124 iuneq1 4733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 𝑗𝑛 (𝑏𝑗) = 𝑗𝑘 (𝑏𝑗))
125123, 124syl5eq 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 𝑘𝑛 (𝑏𝑘) = 𝑗𝑘 (𝑏𝑗))
12661, 125difeq12d 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) = ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)))
127121, 126eleq12d 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ↔ (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
128127rspccv 3506 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑘 ∈ ω → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
12997, 101mpbidi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
13095, 129ralrimi 3152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
131128, 130syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
1321313ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
133 eldifi 3938 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑘) ∈ (𝑏𝑘))
134 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ (𝑏𝑘) ↔ (𝑐𝑛) ∈ (𝑏𝑘)))
135133, 134syl5ib 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
1361353ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
137132, 136syld 47 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑘)))
138137imp 395 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ (𝑏𝑘))
139 ssiun2 4762 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑛 → (𝑏𝑘) ⊆ 𝑘𝑛 (𝑏𝑘))
140139sseld 3804 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑛 → ((𝑐𝑛) ∈ (𝑏𝑘) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
141138, 140syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
1421413impib 1137 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
143129com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
1441433ad2ant2 1157 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
145144imp 395 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
146145eldifbd 3789 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
1471463adant1 1153 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
148142, 147pm2.21dd 186 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1491483exp 1141 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
150 2a1 28 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
151 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑛 → (𝑏𝑗) = (𝑏𝑛))
152151ssiun2s 4763 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑘 → (𝑏𝑛) ⊆ 𝑗𝑘 (𝑏𝑗))
153152sseld 3804 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝑘 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
154102, 153syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
155145, 154syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1561553impib 1137 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
157 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) ↔ (𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
158 eldifn 3939 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
159157, 158syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1601593ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
161132, 160syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
162161a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))))
1631623imp 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
164156, 163pm2.21dd 186 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1651643exp 1141 . . . . . . . . . . . . . . . . . 18 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
166149, 150, 1653jaoi 1545 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
167166com12 32 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
1681673expia 1143 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛))))
169120, 168mpid 44 . . . . . . . . . . . . . 14 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
170169com3r 87 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
171170expd 402 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))))
17295, 116, 171ralrimd 3154 . . . . . . . . . . 11 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
173172ralrimiv 3160 . . . . . . . . . 10 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
1741733ad2ant3 1158 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
175 dff13 6739 . . . . . . . . 9 (𝑐:ω–1-1𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
176115, 174, 175sylanbrc 574 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω–1-1𝐴)
177 19.8a 2218 . . . . . . . 8 (𝑐:ω–1-1𝐴 → ∃𝑐 𝑐:ω–1-1𝐴)
178176, 177syl 17 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∃𝑐 𝑐:ω–1-1𝐴)
1792brdom 8207 . . . . . . 7 (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1𝐴)
180178, 179sylibr 225 . . . . . 6 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴)
1811803expib 1145 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
182181exlimdv 2024 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
18393, 182mpd 15 . . 3 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
184183exlimiv 2021 . 2 (∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
18548, 184syl 17 1 𝐴 ∈ Fin → ω ≼ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3o 1099  w3a 1100   = wceq 1637  wex 1859  wcel 2157  {cab 2799  wne 2985  wral 3103  Vcvv 3398  cdif 3773  wss 3776  c0 4123  𝒫 cpw 4358   ciun 4719   class class class wbr 4851  cmpt 4930  dom cdm 5318  Ord word 5942  suc csuc 5945   Fn wfn 6099  wf 6100  1-1wf1 6101  cfv 6104  ωcom 7298  cen 8192  cdom 8193  csdm 8194  Fincfn 8195  cardccrd 9047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cc 9545
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-map 8097  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-card 9051  df-cda 9278
This theorem is referenced by:  domtriom  9553
  Copyright terms: Public domain W3C validator