Metamath Proof Explorer

Theorem domtriomlem

Description: Lemma for domtriom . (Contributed by Mario Carneiro, 9-Feb-2013)

Ref Expression
Hypotheses domtriomlem.1 ⊢ 𝐴 ∈ V
domtriomlem.2 ⊢ 𝐵 = { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) }
domtriomlem.3 ⊢ 𝐶 = ( 𝑛 ∈ ω ↦ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
Assertion domtriomlem ( ¬ 𝐴 ∈ Fin → ω ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 domtriomlem.1 ⊢ 𝐴 ∈ V
2 domtriomlem.2 ⊢ 𝐵 = { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) }
3 domtriomlem.3 ⊢ 𝐶 = ( 𝑛 ∈ ω ↦ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
4 1 pwex ⊢ 𝒫 𝐴 ∈ V
5 simpl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) → 𝑦 ⊆ 𝐴 )
6 5 ss2abi ⊢ { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) } ⊆ { 𝑦 ∣ 𝑦 ⊆ 𝐴 }
7 df-pw ⊢ 𝒫 𝐴 = { 𝑦 ∣ 𝑦 ⊆ 𝐴 }
8 6 7 sseqtrri ⊢ { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) } ⊆ 𝒫 𝐴
9 4 8 ssexi ⊢ { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) } ∈ V
10 2 9 eqeltri ⊢ 𝐵 ∈ V
11 omex ⊢ ω ∈ V
12 11 enref ⊢ ω ≈ ω
13 10 12 axcc3 ⊢ ∃ 𝑏 ( 𝑏 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
14 nfv ⊢ Ⅎ 𝑛 ¬ 𝐴 ∈ Fin
15 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
16 14 15 nfan ⊢ Ⅎ 𝑛 ( ¬ 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
17 nnfi ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ Fin )
18 pwfi ⊢ ( 𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin )
19 17 18 sylib ⊢ ( 𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin )
20 ficardom ⊢ ( 𝒫 𝑛 ∈ Fin → ( card ‘ 𝒫 𝑛 ) ∈ ω )
21 isinf ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑚 ∈ ω ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚 ) )
22 breq2 ⊢ ( 𝑚 = ( card ‘ 𝒫 𝑛 ) → ( 𝑦 ≈ 𝑚 ↔ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) )
23 22 anbi2d ⊢ ( 𝑚 = ( card ‘ 𝒫 𝑛 ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) ) )
24 23 exbidv ⊢ ( 𝑚 = ( card ‘ 𝒫 𝑛 ) → ( ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) ) )
25 24 rspcv ⊢ ( ( card ‘ 𝒫 𝑛 ) ∈ ω → ( ∀ 𝑚 ∈ ω ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) ) )
26 21 25 syl5 ⊢ ( ( card ‘ 𝒫 𝑛 ) ∈ ω → ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) ) )
27 19 20 26 3syl ⊢ ( 𝑛 ∈ ω → ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) ) )
28 finnum ⊢ ( 𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card )
29 cardid2 ⊢ ( 𝒫 𝑛 ∈ dom card → ( card ‘ 𝒫 𝑛 ) ≈ 𝒫 𝑛 )
30 entr ⊢ ( ( 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ∧ ( card ‘ 𝒫 𝑛 ) ≈ 𝒫 𝑛 ) → 𝑦 ≈ 𝒫 𝑛 )
31 30 expcom ⊢ ( ( card ‘ 𝒫 𝑛 ) ≈ 𝒫 𝑛 → ( 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) → 𝑦 ≈ 𝒫 𝑛 ) )
32 19 28 29 31 4syl ⊢ ( 𝑛 ∈ ω → ( 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) → 𝑦 ≈ 𝒫 𝑛 ) )
33 32 anim2d ⊢ ( 𝑛 ∈ ω → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) → ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) ) )
34 33 eximdv ⊢ ( 𝑛 ∈ ω → ( ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ ( card ‘ 𝒫 𝑛 ) ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) ) )
35 27 34 syld ⊢ ( 𝑛 ∈ ω → ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) ) )
36 2 neeq1i ⊢ ( 𝐵 ≠ ∅ ↔ { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) } ≠ ∅ )
37 abn0 ⊢ ( { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) } ≠ ∅ ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) )
38 36 37 bitri ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) )
39 35 38 syl6ibr ⊢ ( 𝑛 ∈ ω → ( ¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅ ) )
40 39 com12 ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑛 ∈ ω → 𝐵 ≠ ∅ ) )
41 40 adantr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ( 𝑛 ∈ ω → 𝐵 ≠ ∅ ) )
42 rsp ⊢ ( ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) → ( 𝑛 ∈ ω → ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) )
43 42 adantl ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ( 𝑛 ∈ ω → ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) )
44 41 43 mpdd ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ( 𝑛 ∈ ω → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
45 16 44 ralrimi ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
46 45 3adant2 ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
47 46 3expib ⊢ ( ¬ 𝐴 ∈ Fin → ( ( 𝑏 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
48 47 eximdv ⊢ ( ¬ 𝐴 ∈ Fin → ( ∃ 𝑏 ( 𝑏 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝐵 ≠ ∅ → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) ) → ∃ 𝑏 ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
49 13 48 mpi ⊢ ( ¬ 𝐴 ∈ Fin → ∃ 𝑏 ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
50 axcc2 ⊢ ∃ 𝑐 ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
51 simp2 ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → 𝑐 Fn ω )
52 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵
53 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) )
54 52 53 nfan ⊢ Ⅎ 𝑛 ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
55 fvex ⊢ ( 𝑏 ‘ 𝑛 ) ∈ V
56 sseq1 ⊢ ( 𝑦 = ( 𝑏 ‘ 𝑛 ) → ( 𝑦 ⊆ 𝐴 ↔ ( 𝑏 ‘ 𝑛 ) ⊆ 𝐴 ) )
57 breq1 ⊢ ( 𝑦 = ( 𝑏 ‘ 𝑛 ) → ( 𝑦 ≈ 𝒫 𝑛 ↔ ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 ) )
58 56 57 anbi12d ⊢ ( 𝑦 = ( 𝑏 ‘ 𝑛 ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) ↔ ( ( 𝑏 ‘ 𝑛 ) ⊆ 𝐴 ∧ ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 ) ) )
59 55 58 2 elab2 ⊢ ( ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ↔ ( ( 𝑏 ‘ 𝑛 ) ⊆ 𝐴 ∧ ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 ) )
60 59 simprbi ⊢ ( ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 )
61 60 ralimi ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 )
62 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑏 ‘ 𝑛 ) = ( 𝑏 ‘ 𝑘 ) )
63 pweq ⊢ ( 𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘 )
64 62 63 breq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 ↔ ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 ) )
65 64 cbvralvw ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 ↔ ∀ 𝑘 ∈ ω ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 )
66 peano2 ⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
67 omelon ⊢ ω ∈ On
68 67 onelssi ⊢ ( suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω )
69 ssralv ⊢ ( suc 𝑛 ⊆ ω → ( ∀ 𝑘 ∈ ω ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 → ∀ 𝑘 ∈ suc 𝑛 ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 ) )
70 66 68 69 3syl ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ ω ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 → ∀ 𝑘 ∈ suc 𝑛 ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 ) )
71 pwsdompw ⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑘 ∈ suc 𝑛 ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 ) → ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ≺ ( 𝑏 ‘ 𝑛 ) )
72 71 ex ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ suc 𝑛 ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ≺ ( 𝑏 ‘ 𝑛 ) ) )
73 70 72 syld ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ ω ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ≺ ( 𝑏 ‘ 𝑛 ) ) )
74 sdomdif ⊢ ( ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ≺ ( 𝑏 ‘ 𝑛 ) → ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ≠ ∅ )
75 73 74 syl6 ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ ω ( 𝑏 ‘ 𝑘 ) ≈ 𝒫 𝑘 → ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ≠ ∅ ) )
76 65 75 syl5bi ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 → ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ≠ ∅ ) )
77 55 difexi ⊢ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ∈ V
78 3 fvmpt2 ⊢ ( ( 𝑛 ∈ ω ∧ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ∈ V ) → ( 𝐶 ‘ 𝑛 ) = ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
79 77 78 mpan2 ⊢ ( 𝑛 ∈ ω → ( 𝐶 ‘ 𝑛 ) = ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
80 79 neeq1d ⊢ ( 𝑛 ∈ ω → ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ ↔ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ≠ ∅ ) )
81 76 80 sylibrd ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ≈ 𝒫 𝑛 → ( 𝐶 ‘ 𝑛 ) ≠ ∅ ) )
82 61 81 syl5com ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑛 ∈ ω → ( 𝐶 ‘ 𝑛 ) ≠ ∅ ) )
83 82 adantr ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ( 𝑛 ∈ ω → ( 𝐶 ‘ 𝑛 ) ≠ ∅ ) )
84 rsp ⊢ ( ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑛 ∈ ω → ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) )
85 84 adantl ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ( 𝑛 ∈ ω → ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) )
86 83 85 mpdd ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ( 𝑛 ∈ ω → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
87 54 86 ralrimi ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) )
88 87 3adant2 ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) )
89 51 88 jca ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
90 89 3expib ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) )
91 90 eximdv ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ∃ 𝑐 ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐶 ‘ 𝑛 ) ≠ ∅ → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) → ∃ 𝑐 ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) ) )
92 50 91 mpi ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ∃ 𝑐 ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
93 simp2 ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → 𝑐 Fn ω )
94 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 )
95 52 94 nfan ⊢ Ⅎ 𝑛 ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) )
96 rsp ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑛 ∈ ω → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
97 96 com12 ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) )
98 rsp ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑛 ∈ ω → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
99 98 com12 ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
100 79 eleq2d ⊢ ( 𝑛 ∈ ω → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ↔ ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ) )
101 eldifi ⊢ ( ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑛 ) )
102 100 101 syl6bi ⊢ ( 𝑛 ∈ ω → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑛 ) ) )
103 59 simplbi ⊢ ( ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑏 ‘ 𝑛 ) ⊆ 𝐴 )
104 103 sseld ⊢ ( ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) )
105 102 104 syl9 ⊢ ( 𝑛 ∈ ω → ( ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) ) )
106 99 105 syld ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) ) )
107 106 com23 ⊢ ( 𝑛 ∈ ω → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) ) )
108 97 107 syld ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) ) )
109 108 com13 ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑛 ∈ ω → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) ) )
110 109 imp ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑛 ∈ ω → ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) )
111 95 110 ralrimi ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 )
112 111 3adant2 ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 )
113 ffnfv ⊢ ( 𝑐 : ω ⟶ 𝐴 ↔ ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ 𝐴 ) )
114 93 112 113 sylanbrc ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → 𝑐 : ω ⟶ 𝐴 )
115 nfv ⊢ Ⅎ 𝑛 𝑘 ∈ ω
116 nnord ⊢ ( 𝑘 ∈ ω → Ord 𝑘 )
117 nnord ⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
118 ordtri3or ⊢ ( ( Ord 𝑘 ∧ Ord 𝑛 ) → ( 𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘 ) )
119 116 117 118 syl2an ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘 ) )
120 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑐 ‘ 𝑛 ) = ( 𝑐 ‘ 𝑘 ) )
121 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑗 ) )
122 121 cbviunv ⊢ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) = ∪ 𝑗 ∈ 𝑛 ( 𝑏 ‘ 𝑗 )
123 iuneq1 ⊢ ( 𝑛 = 𝑘 → ∪ 𝑗 ∈ 𝑛 ( 𝑏 ‘ 𝑗 ) = ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) )
124 122 123 eqtrid ⊢ ( 𝑛 = 𝑘 → ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) = ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) )
125 62 124 difeq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
126 120 125 eleq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ↔ ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ) )
127 126 rspccv ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) → ( 𝑘 ∈ ω → ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ) )
128 96 100 mpbidi ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑛 ∈ ω → ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ) )
129 94 128 ralrimi ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
130 127 129 syl11 ⊢ ( 𝑘 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ) )
131 130 3ad2ant1 ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ) )
132 eldifi ⊢ ( ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ( 𝑏 ‘ 𝑘 ) )
133 eleq1 ⊢ ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → ( ( 𝑐 ‘ 𝑘 ) ∈ ( 𝑏 ‘ 𝑘 ) ↔ ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑘 ) ) )
134 132 133 syl5ib ⊢ ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → ( ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑘 ) ) )
135 134 3ad2ant3 ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑘 ) ) )
136 131 135 syld ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑘 ) ) )
137 136 imp ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑘 ) )
138 ssiun2 ⊢ ( 𝑘 ∈ 𝑛 → ( 𝑏 ‘ 𝑘 ) ⊆ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
139 138 sseld ⊢ ( 𝑘 ∈ 𝑛 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑘 ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
140 137 139 syl5 ⊢ ( 𝑘 ∈ 𝑛 → ( ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
141 140 3impib ⊢ ( ( 𝑘 ∈ 𝑛 ∧ ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
142 128 com12 ⊢ ( 𝑛 ∈ ω → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ) )
143 142 3ad2ant2 ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) ) )
144 143 imp ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
145 144 eldifbd ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
146 145 3adant1 ⊢ ( ( 𝑘 ∈ 𝑛 ∧ ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
147 141 146 pm2.21dd ⊢ ( ( 𝑘 ∈ 𝑛 ∧ ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → 𝑘 = 𝑛 )
148 147 3exp ⊢ ( 𝑘 ∈ 𝑛 → ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
149 2a1 ⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
150 fveq2 ⊢ ( 𝑗 = 𝑛 → ( 𝑏 ‘ 𝑗 ) = ( 𝑏 ‘ 𝑛 ) )
151 150 ssiun2s ⊢ ( 𝑛 ∈ 𝑘 → ( 𝑏 ‘ 𝑛 ) ⊆ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) )
152 151 sseld ⊢ ( 𝑛 ∈ 𝑘 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( 𝑏 ‘ 𝑛 ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
153 101 152 syl5 ⊢ ( 𝑛 ∈ 𝑘 → ( ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
154 144 153 syl5 ⊢ ( 𝑛 ∈ 𝑘 → ( ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
155 154 3impib ⊢ ( ( 𝑛 ∈ 𝑘 ∧ ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) )
156 eleq1 ⊢ ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → ( ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ↔ ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ) )
157 eldifn ⊢ ( ( 𝑐 ‘ 𝑛 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) )
158 156 157 syl6bi ⊢ ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → ( ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
159 158 3ad2ant3 ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ( 𝑐 ‘ 𝑘 ) ∈ ( ( 𝑏 ‘ 𝑘 ) ∖ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
160 131 159 syld ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) )
161 160 a1i ⊢ ( 𝑛 ∈ 𝑘 → ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) ) ) )
162 161 3imp ⊢ ( ( 𝑛 ∈ 𝑘 ∧ ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ¬ ( 𝑐 ‘ 𝑛 ) ∈ ∪ 𝑗 ∈ 𝑘 ( 𝑏 ‘ 𝑗 ) )
163 155 162 pm2.21dd ⊢ ( ( 𝑛 ∈ 𝑘 ∧ ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → 𝑘 = 𝑛 )
164 163 3exp ⊢ ( 𝑛 ∈ 𝑘 → ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
165 148 149 164 3jaoi ⊢ ( ( 𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘 ) → ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
166 165 com12 ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) ) → ( ( 𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘 ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
167 166 3expia ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ) → ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘 ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) ) )
168 119 167 mpid ⊢ ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ) → ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
169 168 com3r ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( ( 𝑘 ∈ ω ∧ 𝑛 ∈ ω ) → ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
170 169 expd ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑘 ∈ ω → ( 𝑛 ∈ ω → ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) ) )
171 94 115 170 ralrimd ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ( 𝑘 ∈ ω → ∀ 𝑛 ∈ ω ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
172 171 ralrimiv ⊢ ( ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) → ∀ 𝑘 ∈ ω ∀ 𝑛 ∈ ω ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → 𝑘 = 𝑛 ) )
173 172 3ad2ant3 ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ∀ 𝑘 ∈ ω ∀ 𝑛 ∈ ω ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → 𝑘 = 𝑛 ) )
174 dff13 ⊢ ( 𝑐 : ω –1-1→ 𝐴 ↔ ( 𝑐 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ∀ 𝑛 ∈ ω ( ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑛 ) → 𝑘 = 𝑛 ) ) )
175 114 173 174 sylanbrc ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → 𝑐 : ω –1-1→ 𝐴 )
176 175 19.8ad ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑐 𝑐 : ω –1-1→ 𝐴 )
177 1 brdom ⊢ ( ω ≼ 𝐴 ↔ ∃ 𝑐 𝑐 : ω –1-1→ 𝐴 )
178 176 177 sylibr ⊢ ( ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ω ≼ 𝐴 )
179 178 3expib ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ω ≼ 𝐴 ) )
180 179 exlimdv ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ( ∃ 𝑐 ( 𝑐 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝑐 ‘ 𝑛 ) ∈ ( 𝐶 ‘ 𝑛 ) ) → ω ≼ 𝐴 ) )
181 92 180 mpd ⊢ ( ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ω ≼ 𝐴 )
182 181 exlimiv ⊢ ( ∃ 𝑏 ∀ 𝑛 ∈ ω ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 → ω ≼ 𝐴 )
183 49 182 syl ⊢ ( ¬ 𝐴 ∈ Fin → ω ≼ 𝐴 )