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

Theorem domtriomlem 9147
 Description: Lemma for domtriom 9148. (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 4774 . . . . . 6 𝒫 𝐴 ∈ V
4 simpl 472 . . . . . . . 8 ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) → 𝑦𝐴)
54ss2abi 3637 . . . . . . 7 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦𝑦𝐴}
6 df-pw 4110 . . . . . . 7 𝒫 𝐴 = {𝑦𝑦𝐴}
75, 6sseqtr4i 3601 . . . . . 6 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
83, 7ssexi 4731 . . . . 5 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ∈ V
91, 8eqeltri 2684 . . . 4 𝐵 ∈ V
10 omex 8423 . . . . 5 ω ∈ V
1110enref 7874 . . . 4 ω ≈ ω
129, 11axcc3 9143 . . 3 𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
13 nfv 1830 . . . . . . . 8 𝑛 ¬ 𝐴 ∈ Fin
14 nfra1 2925 . . . . . . . 8 𝑛𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)
1513, 14nfan 1816 . . . . . . 7 𝑛𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
16 nnfi 8038 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → 𝑛 ∈ Fin)
17 pwfi 8144 . . . . . . . . . . . . . 14 (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
1816, 17sylib 207 . . . . . . . . . . . . 13 (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19 ficardom 8670 . . . . . . . . . . . . 13 (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20 isinf 8058 . . . . . . . . . . . . . 14 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚))
21 breq2 4587 . . . . . . . . . . . . . . . . 17 (𝑚 = (card‘𝒫 𝑛) → (𝑦𝑚𝑦 ≈ (card‘𝒫 𝑛)))
2221anbi2d 736 . . . . . . . . . . . . . . . 16 (𝑚 = (card‘𝒫 𝑛) → ((𝑦𝐴𝑦𝑚) ↔ (𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2322exbidv 1837 . . . . . . . . . . . . . . 15 (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦𝐴𝑦𝑚) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2423rspcv 3278 . . . . . . . . . . . . . 14 ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2520, 24syl5 33 . . . . . . . . . . . . 13 ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2618, 19, 253syl 18 . . . . . . . . . . . 12 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
27 finnum 8657 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28 cardid2 8662 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29 entr 7894 . . . . . . . . . . . . . . . 16 ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
3029expcom 450 . . . . . . . . . . . . . . 15 ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3231anim2d 587 . . . . . . . . . . . . 13 (𝑛 ∈ ω → ((𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3332eximdv 1833 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3426, 33syld 46 . . . . . . . . . . 11 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
351neeq1i 2846 . . . . . . . . . . . 12 (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36 abn0 3908 . . . . . . . . . . . 12 ({𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3735, 36bitri 263 . . . . . . . . . . 11 (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3834, 37syl6ibr 241 . . . . . . . . . 10 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
3938com12 32 . . . . . . . . 9 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
4039adantr 480 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41 rsp 2913 . . . . . . . . 9 (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4241adantl 481 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4340, 42mpdd 42 . . . . . . 7 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
4415, 43ralrimi 2940 . . . . . 6 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
45443adant2 1073 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
46453expib 1260 . . . 4 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4746eximdv 1833 . . 3 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4812, 47mpi 20 . 2 𝐴 ∈ Fin → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
49 axcc2 9142 . . . . 5 𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
50 simp2 1055 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → 𝑐 Fn ω)
51 nfra1 2925 . . . . . . . . . . 11 𝑛𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵
52 nfra1 2925 . . . . . . . . . . 11 𝑛𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))
5351, 52nfan 1816 . . . . . . . . . 10 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
54 fvex 6113 . . . . . . . . . . . . . . . 16 (𝑏𝑛) ∈ V
55 sseq1 3589 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦𝐴 ↔ (𝑏𝑛) ⊆ 𝐴))
56 breq1 4586 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏𝑛) ≈ 𝒫 𝑛))
5755, 56anbi12d 743 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏𝑛) → ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛)))
5854, 57, 1elab2 3323 . . . . . . . . . . . . . . 15 ((𝑏𝑛) ∈ 𝐵 ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛))
5958simprbi 479 . . . . . . . . . . . . . 14 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ≈ 𝒫 𝑛)
6059ralimi 2936 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛)
61 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑏𝑛) = (𝑏𝑘))
62 pweq 4111 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
6361, 62breq12d 4596 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ((𝑏𝑛) ≈ 𝒫 𝑛 ↔ (𝑏𝑘) ≈ 𝒫 𝑘))
6463cbvralv 3147 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘)
65 peano2 6978 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66 omelon 8426 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
6766onelssi 5753 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68 ssralv 3629 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
6965, 67, 683syl 18 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
70 pwsdompw 8909 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘) → 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛))
7170ex 449 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
7269, 71syld 46 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
73 sdomdif 7993 . . . . . . . . . . . . . . . 16 ( 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛) → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅)
7472, 73syl6 34 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7564, 74syl5bi 231 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
76 difss 3699 . . . . . . . . . . . . . . . . 17 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ⊆ (𝑏𝑛)
7754, 76ssexi 4731 . . . . . . . . . . . . . . . 16 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V
78 domtriomlem.3 . . . . . . . . . . . . . . . . 17 𝐶 = (𝑛 ∈ ω ↦ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7978fvmpt2 6200 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V) → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8077, 79mpan2 703 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8180neeq1d 2841 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ ↔ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
8275, 81sylibrd 248 . . . . . . . . . . . . 13 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → (𝐶𝑛) ≠ ∅))
8360, 82syl5com 31 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
8483adantr 480 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
85 rsp 2913 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8685adantl 481 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8784, 86mpdd 42 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
8853, 87ralrimi 2940 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
89883adant2 1073 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
9050, 89jca 553 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
91903expib 1260 . . . . . 6 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9291eximdv 1833 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9349, 92mpi 20 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
94 simp2 1055 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐 Fn ω)
95 nfra1 2925 . . . . . . . . . . . . 13 𝑛𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)
9651, 95nfan 1816 . . . . . . . . . . . 12 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
97 rsp 2913 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
9897com12 32 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝐶𝑛)))
99 rsp 2913 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
10099com12 32 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ∈ 𝐵))
10180eleq2d 2673 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) ↔ (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
102 eldifi 3694 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ (𝑏𝑛))
103101, 102syl6bi 242 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑛)))
10458simplbi 475 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ⊆ 𝐴)
105104sseld 3567 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝐴))
106103, 105syl9 75 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
107100, 106syld 46 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
108107com23 84 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
10998, 108syld 46 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
110109com13 86 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴)))
111110imp 444 . . . . . . . . . . . 12 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴))
11296, 111ralrimi 2940 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
1131123adant2 1073 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
114 ffnfv 6295 . . . . . . . . . 10 (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴))
11594, 113, 114sylanbrc 695 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω⟶𝐴)
116 nfv 1830 . . . . . . . . . . . 12 𝑛 𝑘 ∈ ω
117 nnord 6965 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
118 nnord 6965 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → Ord 𝑛)
119 ordtri3or 5672 . . . . . . . . . . . . . . . 16 ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
120117, 118, 119syl2an 493 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
12197, 101mpbidi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
12295, 121ralrimi 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
123 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝑐𝑛) = (𝑐𝑘))
124 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑗 → (𝑏𝑘) = (𝑏𝑗))
125124cbviunv 4495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑘𝑛 (𝑏𝑘) = 𝑗𝑛 (𝑏𝑗)
126 iuneq1 4470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 𝑗𝑛 (𝑏𝑗) = 𝑗𝑘 (𝑏𝑗))
127125, 126syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 𝑘𝑛 (𝑏𝑘) = 𝑗𝑘 (𝑏𝑗))
12861, 127difeq12d 3691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) = ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)))
129123, 128eleq12d 2682 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ↔ (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
130129rspccv 3279 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑘 ∈ ω → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
131122, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
132131com12 32 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
1331323ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
134 eldifi 3694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑘) ∈ (𝑏𝑘))
135 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ (𝑏𝑘) ↔ (𝑐𝑛) ∈ (𝑏𝑘)))
136134, 135syl5ib 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
1371363ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
138133, 137syld 46 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑘)))
139138imp 444 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ (𝑏𝑘))
140 ssiun2 4499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑛 → (𝑏𝑘) ⊆ 𝑘𝑛 (𝑏𝑘))
141140sseld 3567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑛 → ((𝑐𝑛) ∈ (𝑏𝑘) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
142139, 141syl5 33 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
1431423impib 1254 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
144121com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
1451443ad2ant2 1076 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
146145imp 444 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
147146eldifbd 3553 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
1481473adant1 1072 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
149143, 148pm2.21dd 185 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1501493exp 1256 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
151 2a1 28 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
152 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑛 → (𝑏𝑗) = (𝑏𝑛))
153152ssiun2s 4500 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑘 → (𝑏𝑛) ⊆ 𝑗𝑘 (𝑏𝑗))
154153sseld 3567 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝑘 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
155102, 154syl5 33 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
156146, 155syl5 33 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1571563impib 1254 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
158 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) ↔ (𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
159 eldifn 3695 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
160158, 159syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1611603ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
162133, 161syld 46 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
163162a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))))
1641633imp 1249 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
165157, 164pm2.21dd 185 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1661653exp 1256 . . . . . . . . . . . . . . . . . 18 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
167150, 151, 1663jaoi 1383 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
168167com12 32 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
1691683expia 1259 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛))))
170120, 169mpid 43 . . . . . . . . . . . . . 14 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
171170com3r 85 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
172171expd 451 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))))
17395, 116, 172ralrimd 2942 . . . . . . . . . . 11 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
174173ralrimiv 2948 . . . . . . . . . 10 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
1751743ad2ant3 1077 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
176 dff13 6416 . . . . . . . . 9 (𝑐:ω–1-1𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
177115, 175, 176sylanbrc 695 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω–1-1𝐴)
178 19.8a 2039 . . . . . . . 8 (𝑐:ω–1-1𝐴 → ∃𝑐 𝑐:ω–1-1𝐴)
179177, 178syl 17 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∃𝑐 𝑐:ω–1-1𝐴)
1802brdom 7853 . . . . . . 7 (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1𝐴)
181179, 180sylibr 223 . . . . . 6 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴)
1821813expib 1260 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
183182exlimdv 1848 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
18493, 183mpd 15 . . 3 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
185184exlimiv 1845 . 2 (∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
18648, 185syl 17 1 𝐴 ∈ Fin → ω ≼ 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  Ord word 5639  suc csuc 5642   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  ‘cfv 5804  ωcom 6957   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841  cardccrd 8644 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cc 9140 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873 This theorem is referenced by:  domtriom  9148
 Copyright terms: Public domain W3C validator