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

Theorem domtriomlem 9855
 Description: Lemma for domtriom 9856. (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 5246 . . . . . 6 𝒫 𝐴 ∈ V
4 simpl 486 . . . . . . . 8 ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) → 𝑦𝐴)
54ss2abi 3994 . . . . . . 7 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦𝑦𝐴}
6 df-pw 4499 . . . . . . 7 𝒫 𝐴 = {𝑦𝑦𝐴}
75, 6sseqtrri 3952 . . . . . 6 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
83, 7ssexi 5190 . . . . 5 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ∈ V
91, 8eqeltri 2886 . . . 4 𝐵 ∈ V
10 omex 9092 . . . . 5 ω ∈ V
1110enref 8527 . . . 4 ω ≈ ω
129, 11axcc3 9851 . . 3 𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
13 nfv 1915 . . . . . . . 8 𝑛 ¬ 𝐴 ∈ Fin
14 nfra1 3183 . . . . . . . 8 𝑛𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)
1513, 14nfan 1900 . . . . . . 7 𝑛𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
16 nnfi 8698 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → 𝑛 ∈ Fin)
17 pwfi 8805 . . . . . . . . . . . . . 14 (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
1816, 17sylib 221 . . . . . . . . . . . . 13 (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19 ficardom 9376 . . . . . . . . . . . . 13 (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20 isinf 8717 . . . . . . . . . . . . . 14 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚))
21 breq2 5034 . . . . . . . . . . . . . . . . 17 (𝑚 = (card‘𝒫 𝑛) → (𝑦𝑚𝑦 ≈ (card‘𝒫 𝑛)))
2221anbi2d 631 . . . . . . . . . . . . . . . 16 (𝑚 = (card‘𝒫 𝑛) → ((𝑦𝐴𝑦𝑚) ↔ (𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2322exbidv 1922 . . . . . . . . . . . . . . 15 (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦𝐴𝑦𝑚) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2423rspcv 3566 . . . . . . . . . . . . . 14 ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2520, 24syl5 34 . . . . . . . . . . . . 13 ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2618, 19, 253syl 18 . . . . . . . . . . . 12 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
27 finnum 9363 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28 cardid2 9368 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29 entr 8546 . . . . . . . . . . . . . . . 16 ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
3029expcom 417 . . . . . . . . . . . . . . 15 ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3231anim2d 614 . . . . . . . . . . . . 13 (𝑛 ∈ ω → ((𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3332eximdv 1918 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3426, 33syld 47 . . . . . . . . . . 11 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
351neeq1i 3051 . . . . . . . . . . . 12 (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36 abn0 4290 . . . . . . . . . . . 12 ({𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3735, 36bitri 278 . . . . . . . . . . 11 (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3834, 37syl6ibr 255 . . . . . . . . . 10 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
3938com12 32 . . . . . . . . 9 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
4039adantr 484 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41 rsp 3170 . . . . . . . . 9 (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4241adantl 485 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4340, 42mpdd 43 . . . . . . 7 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
4415, 43ralrimi 3180 . . . . . 6 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
45443adant2 1128 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
46453expib 1119 . . . 4 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4746eximdv 1918 . . 3 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4812, 47mpi 20 . 2 𝐴 ∈ Fin → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
49 axcc2 9850 . . . . 5 𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
50 simp2 1134 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → 𝑐 Fn ω)
51 nfra1 3183 . . . . . . . . . . 11 𝑛𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵
52 nfra1 3183 . . . . . . . . . . 11 𝑛𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))
5351, 52nfan 1900 . . . . . . . . . 10 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
54 fvex 6658 . . . . . . . . . . . . . . . 16 (𝑏𝑛) ∈ V
55 sseq1 3940 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦𝐴 ↔ (𝑏𝑛) ⊆ 𝐴))
56 breq1 5033 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏𝑛) ≈ 𝒫 𝑛))
5755, 56anbi12d 633 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏𝑛) → ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛)))
5854, 57, 1elab2 3618 . . . . . . . . . . . . . . 15 ((𝑏𝑛) ∈ 𝐵 ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛))
5958simprbi 500 . . . . . . . . . . . . . 14 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ≈ 𝒫 𝑛)
6059ralimi 3128 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛)
61 fveq2 6645 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑏𝑛) = (𝑏𝑘))
62 pweq 4513 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
6361, 62breq12d 5043 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ((𝑏𝑛) ≈ 𝒫 𝑛 ↔ (𝑏𝑘) ≈ 𝒫 𝑘))
6463cbvralvw 3396 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘)
65 peano2 7584 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66 omelon 9095 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
6766onelssi 6267 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68 ssralv 3981 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
6965, 67, 683syl 18 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
70 pwsdompw 9617 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘) → 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛))
7170ex 416 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
7269, 71syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
73 sdomdif 8651 . . . . . . . . . . . . . . . 16 ( 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛) → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅)
7472, 73syl6 35 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7564, 74syl5bi 245 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7654difexi 5196 . . . . . . . . . . . . . . . 16 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V
77 domtriomlem.3 . . . . . . . . . . . . . . . . 17 𝐶 = (𝑛 ∈ ω ↦ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7877fvmpt2 6756 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V) → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7976, 78mpan2 690 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8079neeq1d 3046 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ ↔ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
8175, 80sylibrd 262 . . . . . . . . . . . . 13 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → (𝐶𝑛) ≠ ∅))
8260, 81syl5com 31 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
8382adantr 484 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
84 rsp 3170 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8584adantl 485 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8683, 85mpdd 43 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
8753, 86ralrimi 3180 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
88873adant2 1128 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
8950, 88jca 515 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
90893expib 1119 . . . . . 6 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9190eximdv 1918 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9249, 91mpi 20 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
93 simp2 1134 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐 Fn ω)
94 nfra1 3183 . . . . . . . . . . . . 13 𝑛𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)
9551, 94nfan 1900 . . . . . . . . . . . 12 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
96 rsp 3170 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
9796com12 32 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝐶𝑛)))
98 rsp 3170 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
9998com12 32 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ∈ 𝐵))
10079eleq2d 2875 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) ↔ (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
101 eldifi 4054 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ (𝑏𝑛))
102100, 101syl6bi 256 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑛)))
10358simplbi 501 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ⊆ 𝐴)
104103sseld 3914 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝐴))
105102, 104syl9 77 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
10699, 105syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
107106com23 86 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
10897, 107syld 47 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
109108com13 88 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴)))
110109imp 410 . . . . . . . . . . . 12 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴))
11195, 110ralrimi 3180 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
1121113adant2 1128 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
113 ffnfv 6859 . . . . . . . . . 10 (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴))
11493, 112, 113sylanbrc 586 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω⟶𝐴)
115 nfv 1915 . . . . . . . . . . . 12 𝑛 𝑘 ∈ ω
116 nnord 7570 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
117 nnord 7570 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → Ord 𝑛)
118 ordtri3or 6191 . . . . . . . . . . . . . . . 16 ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
119116, 117, 118syl2an 598 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
120 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (𝑐𝑛) = (𝑐𝑘))
121 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑗 → (𝑏𝑘) = (𝑏𝑗))
122121cbviunv 4927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑘𝑛 (𝑏𝑘) = 𝑗𝑛 (𝑏𝑗)
123 iuneq1 4897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 𝑗𝑛 (𝑏𝑗) = 𝑗𝑘 (𝑏𝑗))
124122, 123syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 𝑘𝑛 (𝑏𝑘) = 𝑗𝑘 (𝑏𝑗))
12561, 124difeq12d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) = ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)))
126120, 125eleq12d 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ↔ (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
127126rspccv 3568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑘 ∈ ω → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
12896, 100mpbidi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
12994, 128ralrimi 3180 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
130127, 129syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
1311303ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
132 eldifi 4054 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑘) ∈ (𝑏𝑘))
133 eleq1 2877 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ (𝑏𝑘) ↔ (𝑐𝑛) ∈ (𝑏𝑘)))
134132, 133syl5ib 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
1351343ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
136131, 135syld 47 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑘)))
137136imp 410 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ (𝑏𝑘))
138 ssiun2 4934 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑛 → (𝑏𝑘) ⊆ 𝑘𝑛 (𝑏𝑘))
139138sseld 3914 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑛 → ((𝑐𝑛) ∈ (𝑏𝑘) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
140137, 139syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
1411403impib 1113 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
142128com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
1431423ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
144143imp 410 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
145144eldifbd 3894 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
1461453adant1 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
147141, 146pm2.21dd 198 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1481473exp 1116 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
149 2a1 28 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
150 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑛 → (𝑏𝑗) = (𝑏𝑛))
151150ssiun2s 4935 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑘 → (𝑏𝑛) ⊆ 𝑗𝑘 (𝑏𝑗))
152151sseld 3914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝑘 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
153101, 152syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
154144, 153syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1551543impib 1113 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
156 eleq1 2877 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) ↔ (𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
157 eldifn 4055 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
158156, 157syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1591583ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
160131, 159syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
161160a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))))
1621613imp 1108 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
163155, 162pm2.21dd 198 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1641633exp 1116 . . . . . . . . . . . . . . . . . 18 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
165148, 149, 1643jaoi 1424 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
166165com12 32 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
1671663expia 1118 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛))))
168119, 167mpid 44 . . . . . . . . . . . . . 14 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
169168com3r 87 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
170169expd 419 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))))
17194, 115, 170ralrimd 3182 . . . . . . . . . . 11 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
172171ralrimiv 3148 . . . . . . . . . 10 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
1731723ad2ant3 1132 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
174 dff13 6991 . . . . . . . . 9 (𝑐:ω–1-1𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
175114, 173, 174sylanbrc 586 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω–1-1𝐴)
17617519.8ad 2179 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∃𝑐 𝑐:ω–1-1𝐴)
1772brdom 8506 . . . . . . 7 (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1𝐴)
178176, 177sylibr 237 . . . . . 6 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴)
1791783expib 1119 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
180179exlimdv 1934 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
18192, 180mpd 15 . . 3 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182181exlimiv 1931 . 2 (∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
18348, 182syl 17 1 𝐴 ∈ Fin → ω ≼ 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  ∪ ciun 4881   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  Ord word 6158  suc csuc 6161   Fn wfn 6319  ⟶wf 6320  –1-1→wf1 6321  ‘cfv 6324  ωcom 7562   ≈ cen 8491   ≼ cdom 8492   ≺ csdm 8493  Fincfn 8494  cardccrd 9350 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cc 9848 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-2o 8088  df-oadd 8091  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-dju 9316  df-card 9354 This theorem is referenced by:  domtriom  9856
 Copyright terms: Public domain W3C validator