fseqenlem1

	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⟩\})$
Assertion	fseqenlem1	$⊢ (φ \land C \in ω) \to G (C) : A^{C} \underset{1-1}{⟶} 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		fveq2	$⊢ y = C \to G (y) = G (C)$
6		f1eq1	$⊢ G (y) = G (C) \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (C) : A^{y} \underset{1-1}{⟶} A)$
7	5 6	syl	$⊢ y = C \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (C) : A^{y} \underset{1-1}{⟶} A)$
8		oveq2	$⊢ y = C \to A^{y} = A^{C}$
9		f1eq2	$⊢ A^{y} = A^{C} \to (G (C) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (C) : A^{C} \underset{1-1}{⟶} A)$
10	8 9	syl	$⊢ y = C \to (G (C) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (C) : A^{C} \underset{1-1}{⟶} A)$
11	7 10	bitrd	$⊢ y = C \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (C) : A^{C} \underset{1-1}{⟶} A)$
12	11	imbi2d	$⊢ y = C \to ((φ \to G (y) : A^{y} \underset{1-1}{⟶} A) \leftrightarrow (φ \to G (C) : A^{C} \underset{1-1}{⟶} A))$
13		fveq2	$⊢ y = \emptyset \to G (y) = G (\emptyset)$
14		snex	$⊢ \{⟨\emptyset, B⟩\} \in V$
15	4	seqom0g	$⊢ \{⟨\emptyset, B⟩\} \in V \to G (\emptyset) = \{⟨\emptyset, B⟩\}$
16	14 15	ax-mp	$⊢ G (\emptyset) = \{⟨\emptyset, B⟩\}$
17	13 16	eqtrdi	$⊢ y = \emptyset \to G (y) = \{⟨\emptyset, B⟩\}$
18		f1eq1	$⊢ G (y) = \{⟨\emptyset, B⟩\} \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : A^{y} \underset{1-1}{⟶} A)$
19	17 18	syl	$⊢ y = \emptyset \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : A^{y} \underset{1-1}{⟶} A)$
20		oveq2	$⊢ y = \emptyset \to A^{y} = A^{\emptyset}$
21		f1eq2	$⊢ A^{y} = A^{\emptyset} \to (\{⟨\emptyset, B⟩\} : A^{y} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : A^{\emptyset} \underset{1-1}{⟶} A)$
22	20 21	syl	$⊢ y = \emptyset \to (\{⟨\emptyset, B⟩\} : A^{y} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : A^{\emptyset} \underset{1-1}{⟶} A)$
23	19 22	bitrd	$⊢ y = \emptyset \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : A^{\emptyset} \underset{1-1}{⟶} A)$
24		fveq2	$⊢ y = m \to G (y) = G (m)$
25		f1eq1	$⊢ G (y) = G (m) \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (m) : A^{y} \underset{1-1}{⟶} A)$
26	24 25	syl	$⊢ y = m \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (m) : A^{y} \underset{1-1}{⟶} A)$
27		oveq2	$⊢ y = m \to A^{y} = A^{m}$
28		f1eq2	$⊢ A^{y} = A^{m} \to (G (m) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (m) : A^{m} \underset{1-1}{⟶} A)$
29	27 28	syl	$⊢ y = m \to (G (m) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (m) : A^{m} \underset{1-1}{⟶} A)$
30	26 29	bitrd	$⊢ y = m \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (m) : A^{m} \underset{1-1}{⟶} A)$
31		fveq2	$⊢ y = suc m \to G (y) = G (suc m)$
32		f1eq1	$⊢ G (y) = G (suc m) \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (suc m) : A^{y} \underset{1-1}{⟶} A)$
33	31 32	syl	$⊢ y = suc m \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (suc m) : A^{y} \underset{1-1}{⟶} A)$
34		oveq2	$⊢ y = suc m \to A^{y} = A^{suc m}$
35		f1eq2	$⊢ A^{y} = A^{suc m} \to (G (suc m) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (suc m) : A^{suc m} \underset{1-1}{⟶} A)$
36	34 35	syl	$⊢ y = suc m \to (G (suc m) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (suc m) : A^{suc m} \underset{1-1}{⟶} A)$
37	33 36	bitrd	$⊢ y = suc m \to (G (y) : A^{y} \underset{1-1}{⟶} A \leftrightarrow G (suc m) : A^{suc m} \underset{1-1}{⟶} A)$
38		0ex	$⊢ \emptyset \in V$
39		f1osng	$⊢ (\emptyset \in V \land B \in A) \to \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{B\}$
40	38 2 39	sylancr	$⊢ φ \to \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{B\}$
41		f1of1	$⊢ \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{B\} \to \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} \{B\}$
42	40 41	syl	$⊢ φ \to \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} \{B\}$
43	2	snssd	$⊢ φ \to \{B\} \subseteq A$
44		f1ss	$⊢ (\{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} \{B\} \land \{B\} \subseteq A) \to \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} A$
45	42 43 44	syl2anc	$⊢ φ \to \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} A$
46		map0e	$⊢ A \in V \to A^{\emptyset} = 1_{𝑜}$
47	1 46	syl	$⊢ φ \to A^{\emptyset} = 1_{𝑜}$
48		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
49	47 48	eqtrdi	$⊢ φ \to A^{\emptyset} = \{\emptyset\}$
50		f1eq2	$⊢ A^{\emptyset} = \{\emptyset\} \to (\{⟨\emptyset, B⟩\} : A^{\emptyset} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} A)$
51	49 50	syl	$⊢ φ \to (\{⟨\emptyset, B⟩\} : A^{\emptyset} \underset{1-1}{⟶} A \leftrightarrow \{⟨\emptyset, B⟩\} : \{\emptyset\} \underset{1-1}{⟶} A)$
52	45 51	mpbird	$⊢ φ \to \{⟨\emptyset, B⟩\} : A^{\emptyset} \underset{1-1}{⟶} A$
53	4	seqomsuc	$⊢ m \in ω \to G (suc m) = m (n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))) G (m)$
54	53	ad2antrl	$⊢ (φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \to G (suc m) = m (n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))) G (m)$
55		vex	$⊢ m \in V$
56		fvex	$⊢ G (m) \in V$
57		reseq1	$⊢ x = z \to {x ↾}_{a} = {z ↾}_{a}$
58	57	fveq2d	$⊢ x = z \to b ({x ↾}_{a}) = b ({z ↾}_{a})$
59		fveq1	$⊢ x = z \to x (a) = z (a)$
60	58 59	oveq12d	$⊢ x = z \to b ({x ↾}_{a}) F x (a) = b ({z ↾}_{a}) F z (a)$
61	60	cbvmptv	$⊢ (x \in (A^{suc a}) ⟼ b ({x ↾}_{a}) F x (a)) = (z \in (A^{suc a}) ⟼ b ({z ↾}_{a}) F z (a))$
62		suceq	$⊢ a = m \to suc a = suc m$
63	62	adantr	$⊢ (a = m \land b = G (m)) \to suc a = suc m$
64	63	oveq2d	$⊢ (a = m \land b = G (m)) \to A^{suc a} = A^{suc m}$
65		simpr	$⊢ (a = m \land b = G (m)) \to b = G (m)$
66		reseq2	$⊢ a = m \to {z ↾}_{a} = {z ↾}_{m}$
67	66	adantr	$⊢ (a = m \land b = G (m)) \to {z ↾}_{a} = {z ↾}_{m}$
68	65 67	fveq12d	$⊢ (a = m \land b = G (m)) \to b ({z ↾}_{a}) = G (m) ({z ↾}_{m})$
69		simpl	$⊢ (a = m \land b = G (m)) \to a = m$
70	69	fveq2d	$⊢ (a = m \land b = G (m)) \to z (a) = z (m)$
71	68 70	oveq12d	$⊢ (a = m \land b = G (m)) \to b ({z ↾}_{a}) F z (a) = G (m) ({z ↾}_{m}) F z (m)$
72	64 71	mpteq12dv	$⊢ (a = m \land b = G (m)) \to (z \in (A^{suc a}) ⟼ b ({z ↾}_{a}) F z (a)) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
73	61 72	eqtrid	$⊢ (a = m \land b = G (m)) \to (x \in (A^{suc a}) ⟼ b ({x ↾}_{a}) F x (a)) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
74		nfcv	$⊢ \underline{Ⅎ} a (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))$
75		nfcv	$⊢ \underline{Ⅎ} b (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))$
76		nfcv	$⊢ \underline{Ⅎ} n (x \in (A^{suc a}) ⟼ b ({x ↾}_{a}) F x (a))$
77		nfcv	$⊢ \underline{Ⅎ} f (x \in (A^{suc a}) ⟼ b ({x ↾}_{a}) F x (a))$
78		suceq	$⊢ n = a \to suc n = suc a$
79	78	adantr	$⊢ (n = a \land f = b) \to suc n = suc a$
80	79	oveq2d	$⊢ (n = a \land f = b) \to A^{suc n} = A^{suc a}$
81		simpr	$⊢ (n = a \land f = b) \to f = b$
82		reseq2	$⊢ n = a \to {x ↾}_{n} = {x ↾}_{a}$
83	82	adantr	$⊢ (n = a \land f = b) \to {x ↾}_{n} = {x ↾}_{a}$
84	81 83	fveq12d	$⊢ (n = a \land f = b) \to f ({x ↾}_{n}) = b ({x ↾}_{a})$
85		simpl	$⊢ (n = a \land f = b) \to n = a$
86	85	fveq2d	$⊢ (n = a \land f = b) \to x (n) = x (a)$
87	84 86	oveq12d	$⊢ (n = a \land f = b) \to f ({x ↾}_{n}) F x (n) = b ({x ↾}_{a}) F x (a)$
88	80 87	mpteq12dv	$⊢ (n = a \land f = b) \to (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n)) = (x \in (A^{suc a}) ⟼ b ({x ↾}_{a}) F x (a))$
89	74 75 76 77 88	cbvmpo	$⊢ (n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))) = (a \in V, b \in V ⟼ (x \in (A^{suc a}) ⟼ b ({x ↾}_{a}) F x (a)))$
90		ovex	$⊢ A^{suc m} \in V$
91	90	mptex	$⊢ (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) \in V$
92	73 89 91	ovmpoa	$⊢ (m \in V \land G (m) \in V) \to m (n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))) G (m) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
93	55 56 92	mp2an	$⊢ m (n \in V, f \in V ⟼ (x \in (A^{suc n}) ⟼ f ({x ↾}_{n}) F x (n))) G (m) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
94	54 93	eqtrdi	$⊢ (φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \to G (suc m) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
95	3	ad2antrr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to F : A \times A \underset{1-1 onto}{⟶} A$
96		f1of	$⊢ F : A \times A \underset{1-1 onto}{⟶} A \to F : A \times A ⟶ A$
97	95 96	syl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to F : A \times A ⟶ A$
98		f1f	$⊢ G (m) : A^{m} \underset{1-1}{⟶} A \to G (m) : A^{m} ⟶ A$
99	98	ad2antll	$⊢ (φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \to G (m) : A^{m} ⟶ A$
100	99	adantr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to G (m) : A^{m} ⟶ A$
101		elmapi	$⊢ z \in (A^{suc m}) \to z : suc m ⟶ A$
102	101	adantl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to z : suc m ⟶ A$
103		sssucid	$⊢ m \subseteq suc m$
104		fssres	$⊢ (z : suc m ⟶ A \land m \subseteq suc m) \to ({z ↾}_{m}) : m ⟶ A$
105	102 103 104	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to ({z ↾}_{m}) : m ⟶ A$
106	1	ad2antrr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to A \in V$
107		elmapg	$⊢ (A \in V \land m \in V) \to ({z ↾}_{m} \in (A^{m}) \leftrightarrow ({z ↾}_{m}) : m ⟶ A)$
108	106 55 107	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to ({z ↾}_{m} \in (A^{m}) \leftrightarrow ({z ↾}_{m}) : m ⟶ A)$
109	105 108	mpbird	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to {z ↾}_{m} \in (A^{m})$
110	100 109	ffvelrnd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to G (m) ({z ↾}_{m}) \in A$
111	55	sucid	$⊢ m \in suc m$
112		ffvelrn	$⊢ (z : suc m ⟶ A \land m \in suc m) \to z (m) \in A$
113	102 111 112	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to z (m) \in A$
114	97 110 113	fovrnd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land z \in (A^{suc m})) \to G (m) ({z ↾}_{m}) F z (m) \in A$
115	94 114	fmpt3d	$⊢ (φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \to G (suc m) : A^{suc m} ⟶ A$
116		elmapi	$⊢ a \in (A^{suc m}) \to a : suc m ⟶ A$
117	116	ad2antrl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to a : suc m ⟶ A$
118	117	ffnd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to a Fn suc m$
119		elmapi	$⊢ b \in (A^{suc m}) \to b : suc m ⟶ A$
120	119	ad2antll	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to b : suc m ⟶ A$
121	120	ffnd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to b Fn suc m$
122	103	a1i	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to m \subseteq suc m$
123		fvreseq	$⊢ ((a Fn suc m \land b Fn suc m) \land m \subseteq suc m) \to ({a ↾}_{m} = {b ↾}_{m} \leftrightarrow \forall x \in m a (x) = b (x))$
124	118 121 122 123	syl21anc	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ({a ↾}_{m} = {b ↾}_{m} \leftrightarrow \forall x \in m a (x) = b (x))$
125		fveq2	$⊢ x = m \to a (x) = a (m)$
126		fveq2	$⊢ x = m \to b (x) = b (m)$
127	125 126	eqeq12d	$⊢ x = m \to (a (x) = b (x) \leftrightarrow a (m) = b (m))$
128	55 127	ralsn	$⊢ \forall x \in \{m\} a (x) = b (x) \leftrightarrow a (m) = b (m)$
129	128	bicomi	$⊢ a (m) = b (m) \leftrightarrow \forall x \in \{m\} a (x) = b (x)$
130	129	a1i	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (a (m) = b (m) \leftrightarrow \forall x \in \{m\} a (x) = b (x))$
131	124 130	anbi12d	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (({a ↾}_{m} = {b ↾}_{m} \land a (m) = b (m)) \leftrightarrow (\forall x \in m a (x) = b (x) \land \forall x \in \{m\} a (x) = b (x)))$
132	94	adantr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
133	132	fveq1d	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) (a) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) (a)$
134		reseq1	$⊢ z = a \to {z ↾}_{m} = {a ↾}_{m}$
135	134	fveq2d	$⊢ z = a \to G (m) ({z ↾}_{m}) = G (m) ({a ↾}_{m})$
136		fveq1	$⊢ z = a \to z (m) = a (m)$
137	135 136	oveq12d	$⊢ z = a \to G (m) ({z ↾}_{m}) F z (m) = G (m) ({a ↾}_{m}) F a (m)$
138		eqid	$⊢ (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m))$
139		ovex	$⊢ G (m) ({a ↾}_{m}) F a (m) \in V$
140	137 138 139	fvmpt	$⊢ a \in (A^{suc m}) \to (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) (a) = G (m) ({a ↾}_{m}) F a (m)$
141	140	ad2antrl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) (a) = G (m) ({a ↾}_{m}) F a (m)$
142	133 141	eqtrd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) (a) = G (m) ({a ↾}_{m}) F a (m)$
143		df-ov	$⊢ G (m) ({a ↾}_{m}) F a (m) = F (⟨G (m) ({a ↾}_{m}), a (m)⟩)$
144	142 143	eqtrdi	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) (a) = F (⟨G (m) ({a ↾}_{m}), a (m)⟩)$
145	132	fveq1d	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) (b) = (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) (b)$
146		reseq1	$⊢ z = b \to {z ↾}_{m} = {b ↾}_{m}$
147	146	fveq2d	$⊢ z = b \to G (m) ({z ↾}_{m}) = G (m) ({b ↾}_{m})$
148		fveq1	$⊢ z = b \to z (m) = b (m)$
149	147 148	oveq12d	$⊢ z = b \to G (m) ({z ↾}_{m}) F z (m) = G (m) ({b ↾}_{m}) F b (m)$
150		ovex	$⊢ G (m) ({b ↾}_{m}) F b (m) \in V$
151	149 138 150	fvmpt	$⊢ b \in (A^{suc m}) \to (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) (b) = G (m) ({b ↾}_{m}) F b (m)$
152	151	ad2antll	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (z \in (A^{suc m}) ⟼ G (m) ({z ↾}_{m}) F z (m)) (b) = G (m) ({b ↾}_{m}) F b (m)$
153	145 152	eqtrd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) (b) = G (m) ({b ↾}_{m}) F b (m)$
154		df-ov	$⊢ G (m) ({b ↾}_{m}) F b (m) = F (⟨G (m) ({b ↾}_{m}), b (m)⟩)$
155	153 154	eqtrdi	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (suc m) (b) = F (⟨G (m) ({b ↾}_{m}), b (m)⟩)$
156	144 155	eqeq12d	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (G (suc m) (a) = G (suc m) (b) \leftrightarrow F (⟨G (m) ({a ↾}_{m}), a (m)⟩) = F (⟨G (m) ({b ↾}_{m}), b (m)⟩))$
157	3	ad2antrr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to F : A \times A \underset{1-1 onto}{⟶} A$
158		f1of1	$⊢ F : A \times A \underset{1-1 onto}{⟶} A \to F : A \times A \underset{1-1}{⟶} A$
159	157 158	syl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to F : A \times A \underset{1-1}{⟶} A$
160	99	adantr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (m) : A^{m} ⟶ A$
161		fssres	$⊢ (a : suc m ⟶ A \land m \subseteq suc m) \to ({a ↾}_{m}) : m ⟶ A$
162	117 103 161	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ({a ↾}_{m}) : m ⟶ A$
163	1	ad2antrr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to A \in V$
164		elmapg	$⊢ (A \in V \land m \in V) \to ({a ↾}_{m} \in (A^{m}) \leftrightarrow ({a ↾}_{m}) : m ⟶ A)$
165	163 55 164	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ({a ↾}_{m} \in (A^{m}) \leftrightarrow ({a ↾}_{m}) : m ⟶ A)$
166	162 165	mpbird	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to {a ↾}_{m} \in (A^{m})$
167	160 166	ffvelrnd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (m) ({a ↾}_{m}) \in A$
168		ffvelrn	$⊢ (a : suc m ⟶ A \land m \in suc m) \to a (m) \in A$
169	117 111 168	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to a (m) \in A$
170	167 169	opelxpd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ⟨G (m) ({a ↾}_{m}), a (m)⟩ \in (A \times A)$
171		fssres	$⊢ (b : suc m ⟶ A \land m \subseteq suc m) \to ({b ↾}_{m}) : m ⟶ A$
172	120 103 171	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ({b ↾}_{m}) : m ⟶ A$
173		elmapg	$⊢ (A \in V \land m \in V) \to ({b ↾}_{m} \in (A^{m}) \leftrightarrow ({b ↾}_{m}) : m ⟶ A)$
174	163 55 173	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ({b ↾}_{m} \in (A^{m}) \leftrightarrow ({b ↾}_{m}) : m ⟶ A)$
175	172 174	mpbird	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to {b ↾}_{m} \in (A^{m})$
176	160 175	ffvelrnd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (m) ({b ↾}_{m}) \in A$
177		ffvelrn	$⊢ (b : suc m ⟶ A \land m \in suc m) \to b (m) \in A$
178	120 111 177	sylancl	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to b (m) \in A$
179	176 178	opelxpd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ⟨G (m) ({b ↾}_{m}), b (m)⟩ \in (A \times A)$
180		f1fveq	$⊢ (F : A \times A \underset{1-1}{⟶} A \land (⟨G (m) ({a ↾}_{m}), a (m)⟩ \in (A \times A) \land ⟨G (m) ({b ↾}_{m}), b (m)⟩ \in (A \times A))) \to (F (⟨G (m) ({a ↾}_{m}), a (m)⟩) = F (⟨G (m) ({b ↾}_{m}), b (m)⟩) \leftrightarrow ⟨G (m) ({a ↾}_{m}), a (m)⟩ = ⟨G (m) ({b ↾}_{m}), b (m)⟩)$
181	159 170 179 180	syl12anc	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (F (⟨G (m) ({a ↾}_{m}), a (m)⟩) = F (⟨G (m) ({b ↾}_{m}), b (m)⟩) \leftrightarrow ⟨G (m) ({a ↾}_{m}), a (m)⟩ = ⟨G (m) ({b ↾}_{m}), b (m)⟩)$
182		fvex	$⊢ G (m) ({a ↾}_{m}) \in V$
183		fvex	$⊢ a (m) \in V$
184	182 183	opth	$⊢ ⟨G (m) ({a ↾}_{m}), a (m)⟩ = ⟨G (m) ({b ↾}_{m}), b (m)⟩ \leftrightarrow (G (m) ({a ↾}_{m}) = G (m) ({b ↾}_{m}) \land a (m) = b (m))$
185	181 184	bitrdi	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (F (⟨G (m) ({a ↾}_{m}), a (m)⟩) = F (⟨G (m) ({b ↾}_{m}), b (m)⟩) \leftrightarrow (G (m) ({a ↾}_{m}) = G (m) ({b ↾}_{m}) \land a (m) = b (m)))$
186		simplrr	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to G (m) : A^{m} \underset{1-1}{⟶} A$
187		f1fveq	$⊢ (G (m) : A^{m} \underset{1-1}{⟶} A \land ({a ↾}_{m} \in (A^{m}) \land {b ↾}_{m} \in (A^{m}))) \to (G (m) ({a ↾}_{m}) = G (m) ({b ↾}_{m}) \leftrightarrow {a ↾}_{m} = {b ↾}_{m})$
188	186 166 175 187	syl12anc	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (G (m) ({a ↾}_{m}) = G (m) ({b ↾}_{m}) \leftrightarrow {a ↾}_{m} = {b ↾}_{m})$
189	188	anbi1d	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to ((G (m) ({a ↾}_{m}) = G (m) ({b ↾}_{m}) \land a (m) = b (m)) \leftrightarrow ({a ↾}_{m} = {b ↾}_{m} \land a (m) = b (m)))$
190	156 185 189	3bitrd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (G (suc m) (a) = G (suc m) (b) \leftrightarrow ({a ↾}_{m} = {b ↾}_{m} \land a (m) = b (m)))$
191		eqfnfv	$⊢ (a Fn suc m \land b Fn suc m) \to (a = b \leftrightarrow \forall x \in suc m a (x) = b (x))$
192	118 121 191	syl2anc	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (a = b \leftrightarrow \forall x \in suc m a (x) = b (x))$
193		df-suc	$⊢ suc m = m \cup \{m\}$
194	193	raleqi	$⊢ \forall x \in suc m a (x) = b (x) \leftrightarrow \forall x \in (m \cup \{m\}) a (x) = b (x)$
195		ralunb	$⊢ \forall x \in (m \cup \{m\}) a (x) = b (x) \leftrightarrow (\forall x \in m a (x) = b (x) \land \forall x \in \{m\} a (x) = b (x))$
196	194 195	bitri	$⊢ \forall x \in suc m a (x) = b (x) \leftrightarrow (\forall x \in m a (x) = b (x) \land \forall x \in \{m\} a (x) = b (x))$
197	192 196	bitrdi	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (a = b \leftrightarrow (\forall x \in m a (x) = b (x) \land \forall x \in \{m\} a (x) = b (x)))$
198	131 190 197	3bitr4d	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (G (suc m) (a) = G (suc m) (b) \leftrightarrow a = b)$
199	198	biimpd	$⊢ ((φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \land (a \in (A^{suc m}) \land b \in (A^{suc m}))) \to (G (suc m) (a) = G (suc m) (b) \to a = b)$
200	199	ralrimivva	$⊢ (φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \to \forall a \in (A^{suc m}) \forall b \in (A^{suc m}) (G (suc m) (a) = G (suc m) (b) \to a = b)$
201		dff13	$⊢ G (suc m) : A^{suc m} \underset{1-1}{⟶} A \leftrightarrow (G (suc m) : A^{suc m} ⟶ A \land \forall a \in (A^{suc m}) \forall b \in (A^{suc m}) (G (suc m) (a) = G (suc m) (b) \to a = b))$
202	115 200 201	sylanbrc	$⊢ (φ \land (m \in ω \land G (m) : A^{m} \underset{1-1}{⟶} A)) \to G (suc m) : A^{suc m} \underset{1-1}{⟶} A$
203	202	expr	$⊢ (φ \land m \in ω) \to (G (m) : A^{m} \underset{1-1}{⟶} A \to G (suc m) : A^{suc m} \underset{1-1}{⟶} A)$
204	203	expcom	$⊢ m \in ω \to (φ \to (G (m) : A^{m} \underset{1-1}{⟶} A \to G (suc m) : A^{suc m} \underset{1-1}{⟶} A))$
205	23 30 37 52 204	finds2	$⊢ y \in ω \to (φ \to G (y) : A^{y} \underset{1-1}{⟶} A)$
206	12 205	vtoclga	$⊢ C \in ω \to (φ \to G (C) : A^{C} \underset{1-1}{⟶} A)$
207	206	impcom	$⊢ (φ \land C \in ω) \to G (C) : A^{C} \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem fseqenlem1

Proof