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

Theorem domtriomlem 10056
Description: Lemma for domtriom 10057. (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 5273 . . . . . 6 𝒫 𝐴 ∈ V
4 simpl 486 . . . . . . . 8 ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) → 𝑦𝐴)
54ss2abi 3980 . . . . . . 7 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦𝑦𝐴}
6 df-pw 4515 . . . . . . 7 𝒫 𝐴 = {𝑦𝑦𝐴}
75, 6sseqtrri 3938 . . . . . 6 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
83, 7ssexi 5215 . . . . 5 {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ∈ V
91, 8eqeltri 2834 . . . 4 𝐵 ∈ V
10 omex 9258 . . . . 5 ω ∈ V
1110enref 8661 . . . 4 ω ≈ ω
129, 11axcc3 10052 . . 3 𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
13 nfv 1922 . . . . . . . 8 𝑛 ¬ 𝐴 ∈ Fin
14 nfra1 3140 . . . . . . . 8 𝑛𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)
1513, 14nfan 1907 . . . . . . 7 𝑛𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵))
16 nnfi 8845 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → 𝑛 ∈ Fin)
17 pwfi 8856 . . . . . . . . . . . . . 14 (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
1816, 17sylib 221 . . . . . . . . . . . . 13 (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19 ficardom 9577 . . . . . . . . . . . . 13 (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20 isinf 8891 . . . . . . . . . . . . . 14 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚))
21 breq2 5057 . . . . . . . . . . . . . . . . 17 (𝑚 = (card‘𝒫 𝑛) → (𝑦𝑚𝑦 ≈ (card‘𝒫 𝑛)))
2221anbi2d 632 . . . . . . . . . . . . . . . 16 (𝑚 = (card‘𝒫 𝑛) → ((𝑦𝐴𝑦𝑚) ↔ (𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2322exbidv 1929 . . . . . . . . . . . . . . 15 (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦𝐴𝑦𝑚) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2423rspcv 3532 . . . . . . . . . . . . . 14 ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦𝐴𝑦𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2520, 24syl5 34 . . . . . . . . . . . . 13 ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
2618, 19, 253syl 18 . . . . . . . . . . . 12 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛))))
27 finnum 9564 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28 cardid2 9569 . . . . . . . . . . . . . . 15 (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29 entr 8680 . . . . . . . . . . . . . . . 16 ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
3029expcom 417 . . . . . . . . . . . . . . 15 ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
3231anim2d 615 . . . . . . . . . . . . 13 (𝑛 ∈ ω → ((𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3332eximdv 1925 . . . . . . . . . . . 12 (𝑛 ∈ ω → (∃𝑦(𝑦𝐴𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
3426, 33syld 47 . . . . . . . . . . 11 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛)))
351neeq1i 3005 . . . . . . . . . . . 12 (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36 abn0 4295 . . . . . . . . . . . 12 ({𝑦 ∣ (𝑦𝐴𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3735, 36bitri 278 . . . . . . . . . . 11 (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦𝐴𝑦 ≈ 𝒫 𝑛))
3834, 37syl6ibr 255 . . . . . . . . . 10 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
3938com12 32 . . . . . . . . 9 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
4039adantr 484 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41 rsp 3127 . . . . . . . . 9 (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4241adantl 485 . . . . . . . 8 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)))
4340, 42mpdd 43 . . . . . . 7 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
4415, 43ralrimi 3137 . . . . . 6 ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
45443adant2 1133 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
46453expib 1124 . . . 4 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4746eximdv 1925 . . 3 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏𝑛) ∈ 𝐵)) → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵))
4812, 47mpi 20 . 2 𝐴 ∈ Fin → ∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵)
49 axcc2 10051 . . . . 5 𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
50 simp2 1139 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → 𝑐 Fn ω)
51 nfra1 3140 . . . . . . . . . . 11 𝑛𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵
52 nfra1 3140 . . . . . . . . . . 11 𝑛𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))
5351, 52nfan 1907 . . . . . . . . . 10 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)))
54 fvex 6730 . . . . . . . . . . . . . . . 16 (𝑏𝑛) ∈ V
55 sseq1 3926 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦𝐴 ↔ (𝑏𝑛) ⊆ 𝐴))
56 breq1 5056 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑏𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏𝑛) ≈ 𝒫 𝑛))
5755, 56anbi12d 634 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏𝑛) → ((𝑦𝐴𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛)))
5854, 57, 1elab2 3591 . . . . . . . . . . . . . . 15 ((𝑏𝑛) ∈ 𝐵 ↔ ((𝑏𝑛) ⊆ 𝐴 ∧ (𝑏𝑛) ≈ 𝒫 𝑛))
5958simprbi 500 . . . . . . . . . . . . . 14 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ≈ 𝒫 𝑛)
6059ralimi 3083 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛)
61 fveq2 6717 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑏𝑛) = (𝑏𝑘))
62 pweq 4529 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
6361, 62breq12d 5066 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ((𝑏𝑛) ≈ 𝒫 𝑛 ↔ (𝑏𝑘) ≈ 𝒫 𝑘))
6463cbvralvw 3358 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘)
65 peano2 7668 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66 omelon 9261 . . . . . . . . . . . . . . . . . . 19 ω ∈ On
6766onelssi 6322 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68 ssralv 3967 . . . . . . . . . . . . . . . . . 18 (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
6965, 67, 683syl 18 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘))
70 pwsdompw 9818 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘) → 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛))
7170ex 416 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
7269, 71syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛)))
73 sdomdif 8794 . . . . . . . . . . . . . . . 16 ( 𝑘𝑛 (𝑏𝑘) ≺ (𝑏𝑛) → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅)
7472, 73syl6 35 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏𝑘) ≈ 𝒫 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7564, 74syl5bi 245 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
7654difexi 5221 . . . . . . . . . . . . . . . 16 ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V
77 domtriomlem.3 . . . . . . . . . . . . . . . . 17 𝐶 = (𝑛 ∈ ω ↦ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7877fvmpt2 6829 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ω ∧ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ∈ V) → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
7976, 78mpan2 691 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (𝐶𝑛) = ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
8079neeq1d 3000 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ ↔ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ≠ ∅))
8175, 80sylibrd 262 . . . . . . . . . . . . 13 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ≈ 𝒫 𝑛 → (𝐶𝑛) ≠ ∅))
8260, 81syl5com 31 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
8382adantr 484 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝐶𝑛) ≠ ∅))
84 rsp 3127 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8584adantl 485 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))))
8683, 85mpdd 43 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
8753, 86ralrimi 3137 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
88873adant2 1133 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
8950, 88jca 515 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
90893expib 1124 . . . . . 6 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9190eximdv 1925 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶𝑛) ≠ ∅ → (𝑐𝑛) ∈ (𝐶𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))))
9249, 91mpi 20 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)))
93 simp2 1139 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐 Fn ω)
94 nfra1 3140 . . . . . . . . . . . . 13 𝑛𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)
9551, 94nfan 1907 . . . . . . . . . . . 12 𝑛(∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛))
96 rsp 3127 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ (𝐶𝑛)))
9796com12 32 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝐶𝑛)))
98 rsp 3127 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏𝑛) ∈ 𝐵))
9998com12 32 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ∈ 𝐵))
10079eleq2d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) ↔ (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
101 eldifi 4041 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ (𝑏𝑛))
102100, 101syl6bi 256 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑛)))
10358simplbi 501 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑛) ∈ 𝐵 → (𝑏𝑛) ⊆ 𝐴)
104103sseld 3900 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝐴))
105102, 104syl9 77 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ω → ((𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
10699, 105syld 47 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ 𝐴)))
107106com23 86 . . . . . . . . . . . . . . 15 (𝑛 ∈ ω → ((𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
10897, 107syld 47 . . . . . . . . . . . . . 14 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (𝑐𝑛) ∈ 𝐴)))
109108com13 88 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴)))
110109imp 410 . . . . . . . . . . . 12 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑛 ∈ ω → (𝑐𝑛) ∈ 𝐴))
11195, 110ralrimi 3137 . . . . . . . . . . 11 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
1121113adant2 1133 . . . . . . . . . 10 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴)
113 ffnfv 6935 . . . . . . . . . 10 (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ 𝐴))
11493, 112, 113sylanbrc 586 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω⟶𝐴)
115 nfv 1922 . . . . . . . . . . . 12 𝑛 𝑘 ∈ ω
116 nnord 7652 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
117 nnord 7652 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ω → Ord 𝑛)
118 ordtri3or 6245 . . . . . . . . . . . . . . . 16 ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
119116, 117, 118syl2an 599 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘𝑛𝑘 = 𝑛𝑛𝑘))
120 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → (𝑐𝑛) = (𝑐𝑘))
121 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑗 → (𝑏𝑘) = (𝑏𝑗))
122121cbviunv 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑘𝑛 (𝑏𝑘) = 𝑗𝑛 (𝑏𝑗)
123 iuneq1 4920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 𝑗𝑛 (𝑏𝑗) = 𝑗𝑘 (𝑏𝑗))
124122, 123eqtrid 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 𝑘𝑛 (𝑏𝑘) = 𝑗𝑘 (𝑏𝑗))
12561, 124difeq12d 4038 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) = ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)))
126120, 125eleq12d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) ↔ (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
127126rspccv 3534 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑘 ∈ ω → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
12896, 100mpbidi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑛 ∈ ω → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
12994, 128ralrimi 3137 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑛 ∈ ω (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
130127, 129syl11 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
1311303ad2ant1 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
132 eldifi 4041 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑘) ∈ (𝑏𝑘))
133 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ (𝑏𝑘) ↔ (𝑐𝑛) ∈ (𝑏𝑘)))
134132, 133syl5ib 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
1351343ad2ant3 1137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → (𝑐𝑛) ∈ (𝑏𝑘)))
136131, 135syld 47 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ (𝑏𝑘)))
137136imp 410 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ (𝑏𝑘))
138 ssiun2 4956 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑛 → (𝑏𝑘) ⊆ 𝑘𝑛 (𝑏𝑘))
139138sseld 3900 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑛 → ((𝑐𝑛) ∈ (𝑏𝑘) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
140137, 139syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘)))
1411403impib 1118 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
142128com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
1431423ad2ant2 1136 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘))))
144143imp 410 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)))
145144eldifbd 3879 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
1461453adant1 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑘𝑛 (𝑏𝑘))
147141, 146pm2.21dd 198 . . . . . . . . . . . . . . . . . . 19 ((𝑘𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1481473exp 1121 . . . . . . . . . . . . . . . . . 18 (𝑘𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
149 2a1 28 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
150 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑛 → (𝑏𝑗) = (𝑏𝑛))
151150ssiun2s 4957 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑘 → (𝑏𝑛) ⊆ 𝑗𝑘 (𝑏𝑗))
152151sseld 3900 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝑘 → ((𝑐𝑛) ∈ (𝑏𝑛) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
153101, 152syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘 → ((𝑐𝑛) ∈ ((𝑏𝑛) ∖ 𝑘𝑛 (𝑏𝑘)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
154144, 153syl5 34 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1551543impib 1118 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
156 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) ↔ (𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗))))
157 eldifn 4042 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑛) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
158156, 157syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐𝑘) = (𝑐𝑛) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
1591583ad2ant3 1137 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑐𝑘) ∈ ((𝑏𝑘) ∖ 𝑗𝑘 (𝑏𝑗)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
160131, 159syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗)))
161160a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))))
1621613imp 1113 . . . . . . . . . . . . . . . . . . . 20 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ¬ (𝑐𝑛) ∈ 𝑗𝑘 (𝑏𝑗))
163155, 162pm2.21dd 198 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑘 = 𝑛)
1641633exp 1121 . . . . . . . . . . . . . . . . . 18 (𝑛𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
165148, 149, 1643jaoi 1429 . . . . . . . . . . . . . . . . 17 ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
166165com12 32 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐𝑘) = (𝑐𝑛)) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
1671663expia 1123 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → ((𝑘𝑛𝑘 = 𝑛𝑛𝑘) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛))))
168119, 167mpid 44 . . . . . . . . . . . . . 14 ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → 𝑘 = 𝑛)))
169168com3r 87 . . . . . . . . . . . . 13 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
170169expd 419 . . . . . . . . . . . 12 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))))
17194, 115, 170ralrimd 3139 . . . . . . . . . . 11 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
172171ralrimiv 3104 . . . . . . . . . 10 (∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
1731723ad2ant3 1137 . . . . . . . . 9 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛))
174 dff13 7067 . . . . . . . . 9 (𝑐:ω–1-1𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐𝑘) = (𝑐𝑛) → 𝑘 = 𝑛)))
175114, 173, 174sylanbrc 586 . . . . . . . 8 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → 𝑐:ω–1-1𝐴)
17617519.8ad 2179 . . . . . . 7 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ∃𝑐 𝑐:ω–1-1𝐴)
1772brdom 8640 . . . . . . 7 (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1𝐴)
178176, 177sylibr 237 . . . . . 6 ((∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴)
1791783expib 1124 . . . . 5 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
180179exlimdv 1941 . . . 4 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐𝑛) ∈ (𝐶𝑛)) → ω ≼ 𝐴))
18192, 180mpd 15 . . 3 (∀𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182181exlimiv 1938 . 2 (∃𝑏𝑛 ∈ ω (𝑏𝑛) ∈ 𝐵 → ω ≼ 𝐴)
18348, 182syl 17 1 𝐴 ∈ Fin → ω ≼ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3o 1088  w3a 1089   = wceq 1543  wex 1787  wcel 2110  {cab 2714  wne 2940  wral 3061  Vcvv 3408  cdif 3863  wss 3866  c0 4237  𝒫 cpw 4513   ciun 4904   class class class wbr 5053  cmpt 5135  dom cdm 5551  Ord word 6212  suc csuc 6215   Fn wfn 6375  wf 6376  1-1wf1 6377  cfv 6380  ωcom 7644  cen 8623  cdom 8624  csdm 8625  Fincfn 8626  cardccrd 9551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cc 10049
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-oadd 8206  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-dju 9517  df-card 9555
This theorem is referenced by:  domtriom  10057
  Copyright terms: Public domain W3C validator