fseqenlem2

	Ref	Expression
Hypotheses	fseqenlem.a	$⊢ φ \to A \in V$
	fseqenlem.b	$⊢ φ \to B \in A$
	fseqenlem.f	$⊢ φ \to F : A \times A \underset{1-1 onto}{⟶} A$
	fseqenlem.g	$⊢ G = {seq}_{ω} ((n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))), \{⟨\emptyset, B⟩\})$
	fseqenlem.k	$⊢ K = (y \in ⋃_{k \in ω} (A^{k}) ⟼ ⟨dom y, G (dom y) (y)⟩)$
Assertion	fseqenlem2	$⊢ φ \to K : ⋃_{k \in ω} (A^{k}) \underset{1-1}{⟶} ω \times A$

Proof

Step	Hyp	Ref	Expression
1		fseqenlem.a	$⊢ φ \to A \in V$
2		fseqenlem.b	$⊢ φ \to B \in A$
3		fseqenlem.f	$⊢ φ \to F : A \times A \underset{1-1 onto}{⟶} A$
4		fseqenlem.g	$⊢ G = {seq}_{ω} ((n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))), \{⟨\emptyset, B⟩\})$
5		fseqenlem.k	$⊢ K = (y \in ⋃_{k \in ω} (A^{k}) ⟼ ⟨dom y, G (dom y) (y)⟩)$
6		eliun	$⊢ y \in ⋃_{k \in ω} (A^{k}) \leftrightarrow \exists k \in ω y \in (A^{k})$
7		elmapi	$⊢ y \in (A^{k}) \to y : k ⟶ A$
8	7	ad2antll	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to y : k ⟶ A$
9	8	fdmd	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to dom y = k$
10		simprl	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to k \in ω$
11	9 10	eqeltrd	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to dom y \in ω$
12	9	fveq2d	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to G (dom y) = G (k)$
13	12	fveq1d	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to G (dom y) (y) = G (k) (y)$
14	1 2 3 4	fseqenlem1	$⊢ (φ \land k \in ω) \to G (k) : A^{k} \underset{1-1}{⟶} A$
15	14	adantrr	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to G (k) : A^{k} \underset{1-1}{⟶} A$
16		f1f	$⊢ G (k) : A^{k} \underset{1-1}{⟶} A \to G (k) : A^{k} ⟶ A$
17	15 16	syl	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to G (k) : A^{k} ⟶ A$
18		simprr	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to y \in (A^{k})$
19	17 18	ffvelcdmd	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to G (k) (y) \in A$
20	13 19	eqeltrd	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to G (dom y) (y) \in A$
21	11 20	opelxpd	$⊢ (φ \land (k \in ω \land y \in (A^{k}))) \to ⟨dom y, G (dom y) (y)⟩ \in (ω \times A)$
22	21	rexlimdvaa	$⊢ φ \to (\exists k \in ω y \in (A^{k}) \to ⟨dom y, G (dom y) (y)⟩ \in (ω \times A))$
23	6 22	biimtrid	$⊢ φ \to (y \in ⋃_{k \in ω} (A^{k}) \to ⟨dom y, G (dom y) (y)⟩ \in (ω \times A))$
24	23	imp	$⊢ (φ \land y \in ⋃_{k \in ω} (A^{k})) \to ⟨dom y, G (dom y) (y)⟩ \in (ω \times A)$
25	24 5	fmptd	$⊢ φ \to K : ⋃_{k \in ω} (A^{k}) ⟶ ω \times A$
26		ffun	$⊢ K : ⋃_{k \in ω} (A^{k}) ⟶ ω \times A \to Fun K$
27		funbrfv2b	$⊢ Fun K \to (z K w \leftrightarrow (z \in dom K \land K (z) = w))$
28	25 26 27	3syl	$⊢ φ \to (z K w \leftrightarrow (z \in dom K \land K (z) = w))$
29	28	simplbda	$⊢ (φ \land z K w) \to K (z) = w$
30	28	simprbda	$⊢ (φ \land z K w) \to z \in dom K$
31	25	fdmd	$⊢ φ \to dom K = ⋃_{k \in ω} (A^{k})$
32	31	adantr	$⊢ (φ \land z K w) \to dom K = ⋃_{k \in ω} (A^{k})$
33	30 32	eleqtrd	$⊢ (φ \land z K w) \to z \in ⋃_{k \in ω} (A^{k})$
34		dmeq	$⊢ y = z \to dom y = dom z$
35	34	fveq2d	$⊢ y = z \to G (dom y) = G (dom z)$
36		id	$⊢ y = z \to y = z$
37	35 36	fveq12d	$⊢ y = z \to G (dom y) (y) = G (dom z) (z)$
38	34 37	opeq12d	$⊢ y = z \to ⟨dom y, G (dom y) (y)⟩ = ⟨dom z, G (dom z) (z)⟩$
39		opex	$⊢ ⟨dom z, G (dom z) (z)⟩ \in V$
40	38 5 39	fvmpt	$⊢ z \in ⋃_{k \in ω} (A^{k}) \to K (z) = ⟨dom z, G (dom z) (z)⟩$
41	33 40	syl	$⊢ (φ \land z K w) \to K (z) = ⟨dom z, G (dom z) (z)⟩$
42	29 41	eqtr3d	$⊢ (φ \land z K w) \to w = ⟨dom z, G (dom z) (z)⟩$
43	42	fveq2d	$⊢ (φ \land z K w) \to 1^{st} (w) = 1^{st} (⟨dom z, G (dom z) (z)⟩)$
44		vex	$⊢ z \in V$
45	44	dmex	$⊢ dom z \in V$
46		fvex	$⊢ G (dom z) (z) \in V$
47	45 46	op1st	$⊢ 1^{st} (⟨dom z, G (dom z) (z)⟩) = dom z$
48	43 47	eqtrdi	$⊢ (φ \land z K w) \to 1^{st} (w) = dom z$
49	48	fveq2d	$⊢ (φ \land z K w) \to G (1^{st} (w)) = G (dom z)$
50	49	cnveqd	$⊢ (φ \land z K w) \to {G (1^{st} (w))}^{-1} = {G (dom z)}^{-1}$
51	42	fveq2d	$⊢ (φ \land z K w) \to 2^{nd} (w) = 2^{nd} (⟨dom z, G (dom z) (z)⟩)$
52	45 46	op2nd	$⊢ 2^{nd} (⟨dom z, G (dom z) (z)⟩) = G (dom z) (z)$
53	51 52	eqtrdi	$⊢ (φ \land z K w) \to 2^{nd} (w) = G (dom z) (z)$
54	50 53	fveq12d	$⊢ (φ \land z K w) \to {G (1^{st} (w))}^{-1} (2^{nd} (w)) = {G (dom z)}^{-1} (G (dom z) (z))$
55		eliun	$⊢ z \in ⋃_{k \in ω} (A^{k}) \leftrightarrow \exists k \in ω z \in (A^{k})$
56		elmapi	$⊢ z \in (A^{k}) \to z : k ⟶ A$
57	56	adantl	$⊢ (k \in ω \land z \in (A^{k})) \to z : k ⟶ A$
58	57	fdmd	$⊢ (k \in ω \land z \in (A^{k})) \to dom z = k$
59		simpl	$⊢ (k \in ω \land z \in (A^{k})) \to k \in ω$
60	58 59	eqeltrd	$⊢ (k \in ω \land z \in (A^{k})) \to dom z \in ω$
61		simpr	$⊢ (k \in ω \land z \in (A^{k})) \to z \in (A^{k})$
62	58	oveq2d	$⊢ (k \in ω \land z \in (A^{k})) \to A^{dom z} = A^{k}$
63	61 62	eleqtrrd	$⊢ (k \in ω \land z \in (A^{k})) \to z \in (A^{dom z})$
64	60 63	jca	$⊢ (k \in ω \land z \in (A^{k})) \to (dom z \in ω \land z \in (A^{dom z}))$
65	64	rexlimiva	$⊢ \exists k \in ω z \in (A^{k}) \to (dom z \in ω \land z \in (A^{dom z}))$
66	55 65	sylbi	$⊢ z \in ⋃_{k \in ω} (A^{k}) \to (dom z \in ω \land z \in (A^{dom z}))$
67	33 66	syl	$⊢ (φ \land z K w) \to (dom z \in ω \land z \in (A^{dom z}))$
68	67	simpld	$⊢ (φ \land z K w) \to dom z \in ω$
69	1 2 3 4	fseqenlem1	$⊢ (φ \land dom z \in ω) \to G (dom z) : A^{dom z} \underset{1-1}{⟶} A$
70	68 69	syldan	$⊢ (φ \land z K w) \to G (dom z) : A^{dom z} \underset{1-1}{⟶} A$
71		f1f1orn	$⊢ G (dom z) : A^{dom z} \underset{1-1}{⟶} A \to G (dom z) : A^{dom z} \underset{1-1 onto}{⟶} ran G (dom z)$
72	70 71	syl	$⊢ (φ \land z K w) \to G (dom z) : A^{dom z} \underset{1-1 onto}{⟶} ran G (dom z)$
73	67	simprd	$⊢ (φ \land z K w) \to z \in (A^{dom z})$
74		f1ocnvfv1	$⊢ (G (dom z) : A^{dom z} \underset{1-1 onto}{⟶} ran G (dom z) \land z \in (A^{dom z})) \to {G (dom z)}^{-1} (G (dom z) (z)) = z$
75	72 73 74	syl2anc	$⊢ (φ \land z K w) \to {G (dom z)}^{-1} (G (dom z) (z)) = z$
76	54 75	eqtr2d	$⊢ (φ \land z K w) \to z = {G (1^{st} (w))}^{-1} (2^{nd} (w))$
77	76	ex	$⊢ φ \to (z K w \to z = {G (1^{st} (w))}^{-1} (2^{nd} (w)))$
78	77	alrimiv	$⊢ φ \to \forall z (z K w \to z = {G (1^{st} (w))}^{-1} (2^{nd} (w)))$
79		mo2icl	$⊢ \forall z (z K w \to z = {G (1^{st} (w))}^{-1} (2^{nd} (w))) \to \exists^{*} z z K w$
80	78 79	syl	$⊢ φ \to \exists^{*} z z K w$
81	80	alrimiv	$⊢ φ \to \forall w \exists^{*} z z K w$
82		dff12	$⊢ K : ⋃_{k \in ω} (A^{k}) \underset{1-1}{⟶} ω \times A \leftrightarrow (K : ⋃_{k \in ω} (A^{k}) ⟶ ω \times A \land \forall w \exists^{*} z z K w)$
83	25 81 82	sylanbrc	$⊢ φ \to K : ⋃_{k \in ω} (A^{k}) \underset{1-1}{⟶} ω \times A$

Metamath Proof Explorer

Theorem fseqenlem2

Proof