This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fseqenlem2

Description: Lemma for fseqen . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses fseqenlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fseqenlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
fseqenlem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
fseqenlem.g ⊢ 𝐺 = seqω ( ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) , { ⟨ ∅ , 𝐵 ⟩ } )
fseqenlem.k ⊢ 𝐾 = ( 𝑦 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ↦ ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ )
Assertion fseqenlem2 ( 𝜑 → 𝐾 : ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) –1-1→ ( ω × 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fseqenlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 fseqenlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 fseqenlem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐴 ) –1-1-onto→ 𝐴 )
4 fseqenlem.g ⊢ 𝐺 = seqω ( ( 𝑛 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝐴 ↑m suc 𝑛 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑛 ) ) 𝐹 ( 𝑥 ‘ 𝑛 ) ) ) ) , { ⟨ ∅ , 𝐵 ⟩ } )
5 fseqenlem.k ⊢ 𝐾 = ( 𝑦 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ↦ ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ )
6 eliun ⊢ ( 𝑦 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ↔ ∃ 𝑘 ∈ ω 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) )
7 elmapi ⊢ ( 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) → 𝑦 : 𝑘 ⟶ 𝐴 )
8 7 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → 𝑦 : 𝑘 ⟶ 𝐴 )
9 8 fdmd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → dom 𝑦 = 𝑘 )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → 𝑘 ∈ ω )
11 9 10 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → dom 𝑦 ∈ ω )
12 9 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ( 𝐺 ‘ dom 𝑦 ) = ( 𝐺 ‘ 𝑘 ) )
13 12 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑦 ) )
14 1 2 3 4 fseqenlem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ) → ( 𝐺 ‘ 𝑘 ) : ( 𝐴 ↑m 𝑘 ) –1-1→ 𝐴 )
15 14 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ( 𝐺 ‘ 𝑘 ) : ( 𝐴 ↑m 𝑘 ) –1-1→ 𝐴 )
16 f1f ⊢ ( ( 𝐺 ‘ 𝑘 ) : ( 𝐴 ↑m 𝑘 ) –1-1→ 𝐴 → ( 𝐺 ‘ 𝑘 ) : ( 𝐴 ↑m 𝑘 ) ⟶ 𝐴 )
17 15 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ( 𝐺 ‘ 𝑘 ) : ( 𝐴 ↑m 𝑘 ) ⟶ 𝐴 )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) )
19 17 18 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ( ( 𝐺 ‘ 𝑘 ) ‘ 𝑦 ) ∈ 𝐴 )
20 13 19 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ∈ 𝐴 )
21 11 20 opelxpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) ) ) → ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ∈ ( ω × 𝐴 ) )
22 21 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ω 𝑦 ∈ ( 𝐴 ↑m 𝑘 ) → ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ∈ ( ω × 𝐴 ) ) )
23 6 22 biimtrid ⊢ ( 𝜑 → ( 𝑦 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) → ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ∈ ( ω × 𝐴 ) ) )
24 23 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ) → ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ∈ ( ω × 𝐴 ) )
25 24 5 fmptd ⊢ ( 𝜑 → 𝐾 : ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ⟶ ( ω × 𝐴 ) )
26 ffun ⊢ ( 𝐾 : ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ⟶ ( ω × 𝐴 ) → Fun 𝐾 )
27 funbrfv2b ⊢ ( Fun 𝐾 → ( 𝑧 𝐾 𝑤 ↔ ( 𝑧 ∈ dom 𝐾 ∧ ( 𝐾 ‘ 𝑧 ) = 𝑤 ) ) )
28 25 26 27 3syl ⊢ ( 𝜑 → ( 𝑧 𝐾 𝑤 ↔ ( 𝑧 ∈ dom 𝐾 ∧ ( 𝐾 ‘ 𝑧 ) = 𝑤 ) ) )
29 28 simplbda ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 𝐾 ‘ 𝑧 ) = 𝑤 )
30 28 simprbda ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → 𝑧 ∈ dom 𝐾 )
31 25 fdmd ⊢ ( 𝜑 → dom 𝐾 = ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → dom 𝐾 = ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
33 30 32 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → 𝑧 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) )
34 dmeq ⊢ ( 𝑦 = 𝑧 → dom 𝑦 = dom 𝑧 )
35 34 fveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ dom 𝑦 ) = ( 𝐺 ‘ dom 𝑧 ) )
36 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
37 35 36 fveq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) = ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) )
38 34 37 opeq12d ⊢ ( 𝑦 = 𝑧 → ⟨ dom 𝑦 , ( ( 𝐺 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ = ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ )
39 opex ⊢ ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ ∈ V
40 38 5 39 fvmpt ⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) → ( 𝐾 ‘ 𝑧 ) = ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ )
41 33 40 syl ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 𝐾 ‘ 𝑧 ) = ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ )
42 29 41 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → 𝑤 = ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ )
43 42 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 1st ‘ 𝑤 ) = ( 1st ‘ ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ ) )
44 vex ⊢ 𝑧 ∈ V
45 44 dmex ⊢ dom 𝑧 ∈ V
46 fvex ⊢ ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ∈ V
47 45 46 op1st ⊢ ( 1st ‘ ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ ) = dom 𝑧
48 43 47 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 1st ‘ 𝑤 ) = dom 𝑧 )
49 48 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐺 ‘ dom 𝑧 ) )
50 49 cnveqd ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ◡ ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) = ◡ ( 𝐺 ‘ dom 𝑧 ) )
51 42 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 2nd ‘ 𝑤 ) = ( 2nd ‘ ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ ) )
52 45 46 op2nd ⊢ ( 2nd ‘ ⟨ dom 𝑧 , ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ⟩ ) = ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 )
53 51 52 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 2nd ‘ 𝑤 ) = ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) )
54 50 53 fveq12d ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( ◡ ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) ‘ ( 2nd ‘ 𝑤 ) ) = ( ◡ ( 𝐺 ‘ dom 𝑧 ) ‘ ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ) )
55 eliun ⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ↔ ∃ 𝑘 ∈ ω 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) )
56 elmapi ⊢ ( 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) → 𝑧 : 𝑘 ⟶ 𝐴 )
57 56 adantl ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → 𝑧 : 𝑘 ⟶ 𝐴 )
58 57 fdmd ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → dom 𝑧 = 𝑘 )
59 simpl ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → 𝑘 ∈ ω )
60 58 59 eqeltrd ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → dom 𝑧 ∈ ω )
61 simpr ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) )
62 58 oveq2d ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → ( 𝐴 ↑m dom 𝑧 ) = ( 𝐴 ↑m 𝑘 ) )
63 61 62 eleqtrrd ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) )
64 60 63 jca ⊢ ( ( 𝑘 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) ) → ( dom 𝑧 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) ) )
65 64 rexlimiva ⊢ ( ∃ 𝑘 ∈ ω 𝑧 ∈ ( 𝐴 ↑m 𝑘 ) → ( dom 𝑧 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) ) )
66 55 65 sylbi ⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) → ( dom 𝑧 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) ) )
67 33 66 syl ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( dom 𝑧 ∈ ω ∧ 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) ) )
68 67 simpld ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → dom 𝑧 ∈ ω )
69 1 2 3 4 fseqenlem1 ⊢ ( ( 𝜑 ∧ dom 𝑧 ∈ ω ) → ( 𝐺 ‘ dom 𝑧 ) : ( 𝐴 ↑m dom 𝑧 ) –1-1→ 𝐴 )
70 68 69 syldan ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 𝐺 ‘ dom 𝑧 ) : ( 𝐴 ↑m dom 𝑧 ) –1-1→ 𝐴 )
71 f1f1orn ⊢ ( ( 𝐺 ‘ dom 𝑧 ) : ( 𝐴 ↑m dom 𝑧 ) –1-1→ 𝐴 → ( 𝐺 ‘ dom 𝑧 ) : ( 𝐴 ↑m dom 𝑧 ) –1-1-onto→ ran ( 𝐺 ‘ dom 𝑧 ) )
72 70 71 syl ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( 𝐺 ‘ dom 𝑧 ) : ( 𝐴 ↑m dom 𝑧 ) –1-1-onto→ ran ( 𝐺 ‘ dom 𝑧 ) )
73 67 simprd ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) )
74 f1ocnvfv1 ⊢ ( ( ( 𝐺 ‘ dom 𝑧 ) : ( 𝐴 ↑m dom 𝑧 ) –1-1-onto→ ran ( 𝐺 ‘ dom 𝑧 ) ∧ 𝑧 ∈ ( 𝐴 ↑m dom 𝑧 ) ) → ( ◡ ( 𝐺 ‘ dom 𝑧 ) ‘ ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ) = 𝑧 )
75 72 73 74 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → ( ◡ ( 𝐺 ‘ dom 𝑧 ) ‘ ( ( 𝐺 ‘ dom 𝑧 ) ‘ 𝑧 ) ) = 𝑧 )
76 54 75 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑧 𝐾 𝑤 ) → 𝑧 = ( ◡ ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) ‘ ( 2nd ‘ 𝑤 ) ) )
77 76 ex ⊢ ( 𝜑 → ( 𝑧 𝐾 𝑤 → 𝑧 = ( ◡ ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) ‘ ( 2nd ‘ 𝑤 ) ) ) )
78 77 alrimiv ⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 𝐾 𝑤 → 𝑧 = ( ◡ ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) ‘ ( 2nd ‘ 𝑤 ) ) ) )
79 mo2icl ⊢ ( ∀ 𝑧 ( 𝑧 𝐾 𝑤 → 𝑧 = ( ◡ ( 𝐺 ‘ ( 1st ‘ 𝑤 ) ) ‘ ( 2nd ‘ 𝑤 ) ) ) → ∃* 𝑧 𝑧 𝐾 𝑤 )
80 78 79 syl ⊢ ( 𝜑 → ∃* 𝑧 𝑧 𝐾 𝑤 )
81 80 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ∃* 𝑧 𝑧 𝐾 𝑤 )
82 dff12 ⊢ ( 𝐾 : ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) –1-1→ ( ω × 𝐴 ) ↔ ( 𝐾 : ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) ⟶ ( ω × 𝐴 ) ∧ ∀ 𝑤 ∃* 𝑧 𝑧 𝐾 𝑤 ) )
83 25 81 82 sylanbrc ⊢ ( 𝜑 → 𝐾 : ∪ 𝑘 ∈ ω ( 𝐴 ↑m 𝑘 ) –1-1→ ( ω × 𝐴 ) )