Metamath Proof Explorer

Theorem cantnflem1b

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
oemapval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
oemapval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
oemapvali.r ⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
oemapvali.x ⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
cantnflem1.o ⊢ 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
Assertion cantnflem1b ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5 oemapval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6 oemapval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
7 oemapvali.r ⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
8 oemapvali.x ⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
9 cantnflem1.o ⊢ 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
10 simprr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 )
11 9 oicl ⊢ Ord dom 𝑂
12 ovexd ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ∈ V )
13 1 2 3 9 6 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐺 supp ∅ ) ∧ dom 𝑂 ∈ ω ) )
14 13 simpld ⊢ ( 𝜑 → E We ( 𝐺 supp ∅ ) )
15 9 oiiso ⊢ ( ( ( 𝐺 supp ∅ ) ∈ V ∧ E We ( 𝐺 supp ∅ ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
16 12 14 15 syl2anc ⊢ ( 𝜑 → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
17 isof1o ⊢ ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
18 16 17 syl ⊢ ( 𝜑 → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
19 f1ocnv ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) → ◡ 𝑂 : ( 𝐺 supp ∅ ) –1-1-onto→ dom 𝑂 )
20 f1of ⊢ ( ◡ 𝑂 : ( 𝐺 supp ∅ ) –1-1-onto→ dom 𝑂 → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
21 18 19 20 3syl ⊢ ( 𝜑 → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
22 1 2 3 4 5 6 7 8 cantnflem1a ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 supp ∅ ) )
23 21 22 ffvelrnd ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 )
24 ordelon ⊢ ( ( Ord dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ On )
25 11 23 24 sylancr ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ On )
26 11 a1i ⊢ ( 𝜑 → Ord dom 𝑂 )
27 ordelon ⊢ ( ( Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) → suc 𝑢 ∈ On )
28 26 27 sylan ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → suc 𝑢 ∈ On )
29 sucelon ⊢ ( 𝑢 ∈ On ↔ suc 𝑢 ∈ On )
30 28 29 sylibr ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → 𝑢 ∈ On )
31 30 adantrr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑢 ∈ On )
32 ontri1 ⊢ ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ On ∧ 𝑢 ∈ On ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ↔ ¬ 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ) )
33 25 31 32 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ↔ ¬ 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ) )
34 10 33 mpbid ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ¬ 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑋 ) )
35 16 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
36 ordtr ⊢ ( Ord dom 𝑂 → Tr dom 𝑂 )
37 11 36 mp1i ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → Tr dom 𝑂 )
38 simprl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → suc 𝑢 ∈ dom 𝑂 )
39 trsuc ⊢ ( ( Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) → 𝑢 ∈ dom 𝑂 )
40 37 38 39 syl2anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑢 ∈ dom 𝑂 )
41 23 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 )
42 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ) ) → ( 𝑢 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
43 35 40 41 42 syl12anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑢 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
44 fvex ⊢ ( ◡ 𝑂 ‘ 𝑋 ) ∈ V
45 44 epeli ⊢ ( 𝑢 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑋 ) )
46 fvex ⊢ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ V
47 46 epeli ⊢ ( ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) )
48 43 45 47 3bitr3g ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
49 f1ocnvfv2 ⊢ ( ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) ∧ 𝑋 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
50 18 22 49 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
52 51 eleq2d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ 𝑋 ) )
53 48 52 bitrd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ 𝑋 ) )
54 34 53 mtbid ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ¬ ( 𝑂 ‘ 𝑢 ) ∈ 𝑋 )
55 1 2 3 4 5 6 7 8 oemapvali ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
56 55 simp1d ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
57 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ On )
58 3 56 57 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ On )
59 suppssdm ⊢ ( 𝐺 supp ∅ ) ⊆ dom 𝐺
60 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
61 6 60 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
62 61 simpld ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
63 59 62 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
64 63 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
65 9 oif ⊢ 𝑂 : dom 𝑂 ⟶ ( 𝐺 supp ∅ )
66 65 ffvelrni ⊢ ( 𝑢 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑢 ) ∈ ( 𝐺 supp ∅ ) )
67 40 66 syl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ ( 𝐺 supp ∅ ) )
68 64 67 sseldd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ 𝐵 )
69 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝐵 ) → ( 𝑂 ‘ 𝑢 ) ∈ On )
70 3 68 69 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ On )
71 ontri1 ⊢ ( ( 𝑋 ∈ On ∧ ( 𝑂 ‘ 𝑢 ) ∈ On ) → ( 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ ¬ ( 𝑂 ‘ 𝑢 ) ∈ 𝑋 ) )
72 58 70 71 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ ¬ ( 𝑂 ‘ 𝑢 ) ∈ 𝑋 ) )
73 54 72 mpbird ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) )