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→ ( ω × 𝐴 ) )