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

Theorem domtriomlem 9467
Description: Lemma for domtriom 9468. (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 4982 . . . . . 6 𝒫 𝐴 ∈ V
4 simpl 468 . . . . . . . 8 ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) → 𝑦𝐴)
54ss2abi 3824 . . . . . . 7 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦𝑦𝐴}
6 df-pw 4300 . . . . . . 7 𝒫 𝐴 = {𝑦𝑦𝐴}
75, 6sseqtr4i 3788 . . . . . 6 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
83, 7ssexi 4938 . . . . 5 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ∈ V
91, 8eqeltri 2846 . . . 4 𝐵 ∈ V
10 omex 8705 . . . . 5 ω ∈ V
1110enref 8143 . . . 4 ω ≈ ω
129, 11axcc3 9463 . . 3 𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
13 nfv 1995 . . . . . . . 8 𝑛 ¬ 𝐴 ∈ Fin
14 nfra1 3090 . . . . . . . 8 𝑛𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)
1513, 14nfan 1980 . . . . . . 7 𝑛𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
16 nnfi 8310 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → 𝑛 ∈ Fin)
17 pwfi 8418 . . . . . . . . . . . . . 14 (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
1816, 17sylib 208 . . . . . . . . . . . . 13 (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19 ficardom 8988 . . . . . . . . . . . . 13 (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20 isinf 8330 . . . . . . . . . . . . . 14 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚))
21 breq2 4791 . . . . . . . . . . . . . . . . 17 (𝑚 = (card‘𝒫 𝑛) → (𝑦𝑚𝑦 ≈ (card‘𝒫 𝑛)))
2221anbi2d 608 . . . . . . . . . . . . . . . 16 (𝑚 = (card‘𝒫 𝑛) → ((𝑦𝐴𝑦𝑚) ↔ (𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2322exbidv 2002 . . . . . . . . . . . . . . 15 (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦𝐴𝑦𝑚) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2423rspcv 3457 . . . . . . . . . . . . . 14 ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2520, 24syl5 34 . . . . . . . . . . . . 13 ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2618, 19, 253syl 18 . . . . . . . . . . . 12 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
27 finnum 8975 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28 cardid2 8980 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29 entr 8162 . . . . . . . . . . . . . . . 16 ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
3029expcom 398 . . . . . . . . . . . . . . 15 ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3231anim2d 593 . . . . . . . . . . . . 13 (𝑛 ∈ ω → ((𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3332eximdv 1998 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3426, 33syld 47 . . . . . . . . . . 11 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
351neeq1i 3007 . . . . . . . . . . . 12 (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36 abn0 4102 . . . . . . . . . . . 12 ({𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3735, 36bitri 264 . . . . . . . . . . 11 (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3834, 37syl6ibr 242 . . . . . . . . . 10 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
3938com12 32 . . . . . . . . 9 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
4039adantr 466 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41 rsp 3078 . . . . . . . . 9 (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4241adantl 467 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4340, 42mpdd 43 . . . . . . 7 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
4415, 43ralrimi 3106 . . . . . 6 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
45443adant2 1125 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
46453expib 1116 . . . 4 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4746eximdv 1998 . . 3 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4812, 47mpi 20 . 2 𝐴 ∈ Fin → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
49 axcc2 9462 . . . . 5 𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
50 simp2 1131 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → 𝑐 Fn ω)
51 nfra1 3090 . . . . . . . . . . 11 𝑛𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵
52 nfra1 3090 . . . . . . . . . . 11 𝑛𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))
5351, 52nfan 1980 . . . . . . . . . 10 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
54 fvex 6343 . . . . . . . . . . . . . . . 16 (𝑏𝑛) ∈ V
55 sseq1 3776 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦𝐴 ↔ (𝑏𝑛) ⊆ 𝐴))
56 breq1 4790 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏𝑛) ≈ 𝒫 𝑛))
5755, 56anbi12d 610 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏𝑛) → ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛)))
5854, 57, 1elab2 3506 . . . . . . . . . . . . . . 15 ((𝑏𝑛) ∈ 𝐵 ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛))
5958simprbi 480 . . . . . . . . . . . . . 14 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ≈ 𝒫 𝑛)
6059ralimi 3101 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛)
61 fveq2 6333 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑏𝑛) = (𝑏𝑘))
62 pweq 4301 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
6361, 62breq12d 4800 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ((𝑏𝑛) ≈ 𝒫 𝑛 ↔ (𝑏𝑘) ≈ 𝒫 𝑘))
6463cbvralv 3320 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘)
65 peano2 7234 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66 omelon 8708 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
6766onelssi 5980 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68 ssralv 3816 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
6965, 67, 683syl 18 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
70 pwsdompw 9229 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘) → 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛))
7170ex 397 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
7269, 71syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
73 sdomdif 8265 . . . . . . . . . . . . . . . 16 ( 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛) → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅)
7472, 73syl6 35 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7564, 74syl5bi 232 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
76 difss 3889 . . . . . . . . . . . . . . . . 17 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ⊆ (𝑏𝑛)
7754, 76ssexi 4938 . . . . . . . . . . . . . . . 16 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V
78 domtriomlem.3 . . . . . . . . . . . . . . . . 17 𝐶 = (𝑛 ∈ ω ↦ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7978fvmpt2 6434 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V) → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8077, 79mpan2 665 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8180neeq1d 3002 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ ↔ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
8275, 81sylibrd 249 . . . . . . . . . . . . 13 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → (𝐶𝑛) ≠ ∅))
8360, 82syl5com 31 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
8483adantr 466 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
85 rsp 3078 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8685adantl 467 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8784, 86mpdd 43 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
8853, 87ralrimi 3106 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
89883adant2 1125 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
9050, 89jca 497 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
91903expib 1116 . . . . . 6 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9291eximdv 1998 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9349, 92mpi 20 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
94 simp2 1131 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐 Fn ω)
95 nfra1 3090 . . . . . . . . . . . . 13 𝑛𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)
9651, 95nfan 1980 . . . . . . . . . . . 12 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
97 rsp 3078 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
9897com12 32 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝐶𝑛)))
99 rsp 3078 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
10099com12 32 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ∈ 𝐵))
10180eleq2d 2836 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) ↔ (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
102 eldifi 3884 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ (𝑏𝑛))
103101, 102syl6bi 243 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑛)))
10458simplbi 481 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ⊆ 𝐴)
105104sseld 3752 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝐴))
106103, 105syl9 77 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
107100, 106syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
108107com23 86 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
10998, 108syld 47 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
110109com13 88 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴)))
111110imp 393 . . . . . . . . . . . 12 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴))
11296, 111ralrimi 3106 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
1131123adant2 1125 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
114 ffnfv 6531 . . . . . . . . . 10 (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴))
11594, 113, 114sylanbrc 566 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω⟶𝐴)
116 nfv 1995 . . . . . . . . . . . 12 𝑛 𝑘 ∈ ω
117 nnord 7221 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
118 nnord 7221 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → Ord 𝑛)
119 ordtri3or 5899 . . . . . . . . . . . . . . . 16 ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
120117, 118, 119syl2an 577 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
121 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (𝑐𝑛) = (𝑐𝑘))
122 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑗 → (𝑏𝑘) = (𝑏𝑗))
123122cbviunv 4694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑘𝑛 (𝑏𝑘) = 𝑗𝑛 (𝑏𝑗)
124 iuneq1 4669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 𝑗𝑛 (𝑏𝑗) = 𝑗𝑘 (𝑏𝑗))
125123, 124syl5eq 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 𝑘𝑛 (𝑏𝑘) = 𝑗𝑘 (𝑏𝑗))
12661, 125difeq12d 3881 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) = ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)))
127121, 126eleq12d 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ↔ (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
128127rspccv 3458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑘 ∈ ω → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
12997, 101mpbidi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
13095, 129ralrimi 3106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
131128, 130syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
1321313ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
133 eldifi 3884 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑘) ∈ (𝑏𝑘))
134 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ (𝑏𝑘) ↔ (𝑐𝑛) ∈ (𝑏𝑘)))
135133, 134syl5ib 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
1361353ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
137132, 136syld 47 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑘)))
138137imp 393 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ (𝑏𝑘))
139 ssiun2 4698 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑛 → (𝑏𝑘) ⊆ 𝑘𝑛 (𝑏𝑘))
140139sseld 3752 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑛 → ((𝑐𝑛) ∈ (𝑏𝑘) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
141138, 140syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
1421413impib 1108 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
143129com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
1441433ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
145144imp 393 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
146145eldifbd 3737 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
1471463adant1 1124 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
148142, 147pm2.21dd 186 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1491483exp 1112 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
150 2a1 28 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
151 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑛 → (𝑏𝑗) = (𝑏𝑛))
152151ssiun2s 4699 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑘 → (𝑏𝑛) ⊆ 𝑗𝑘 (𝑏𝑗))
153152sseld 3752 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝑘 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
154102, 153syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
155145, 154syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1561553impib 1108 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
157 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) ↔ (𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
158 eldifn 3885 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
159157, 158syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1601593ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
161132, 160syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
162161a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))))
1631623imp 1101 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
164156, 163pm2.21dd 186 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1651643exp 1112 . . . . . . . . . . . . . . . . . 18 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
166149, 150, 1653jaoi 1539 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
167166com12 32 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
1681673expia 1114 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛))))
169120, 168mpid 44 . . . . . . . . . . . . . 14 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
170169com3r 87 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
171170expd 400 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))))
17295, 116, 171ralrimd 3108 . . . . . . . . . . 11 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
173172ralrimiv 3114 . . . . . . . . . 10 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
1741733ad2ant3 1129 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
175 dff13 6656 . . . . . . . . 9 (𝑐:ω–1-1𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
176115, 174, 175sylanbrc 566 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω–1-1𝐴)
177 19.8a 2206 . . . . . . . 8 (𝑐:ω–1-1𝐴 → ∃𝑐 𝑐:ω–1-1𝐴)
178176, 177syl 17 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∃𝑐 𝑐:ω–1-1𝐴)
1792brdom 8122 . . . . . . 7 (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1𝐴)
180178, 179sylibr 224 . . . . . 6 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴)
1811803expib 1116 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
182181exlimdv 2013 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
18393, 182mpd 15 . . 3 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
184183exlimiv 2010 . 2 (∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
18548, 184syl 17 1 𝐴 ∈ Fin → ω ≼ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3o 1070  w3a 1071   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wne 2943  wral 3061  Vcvv 3351  cdif 3721  wss 3724  c0 4064  𝒫 cpw 4298   ciun 4655   class class class wbr 4787  cmpt 4864  dom cdm 5250  Ord word 5866  suc csuc 5869   Fn wfn 6027  wf 6028  1-1wf1 6029  cfv 6032  ωcom 7213  cen 8107  cdom 8108  csdm 8109  Fincfn 8110  cardccrd 8962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cc 9460
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-er 7897  df-map 8012  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-card 8966  df-cda 9193
This theorem is referenced by:  domtriom  9468
  Copyright terms: Public domain W3C validator