seqomlem2

Description: Lemma for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 23-Jun-2015)

		Ref	Expression
	Hypothesis	seqomlem.a	$⊢ Q = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
	Assertion	seqomlem2	$⊢ Q [ω] Fn ω$

Proof

Step	Hyp	Ref	Expression
1		seqomlem.a	$⊢ Q = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
2		frfnom	$⊢ ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) Fn ω$
3	1	reseq1i	$⊢ {Q ↾}_{ω} = {rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}$
4	3	fneq1i	$⊢ ({Q ↾}_{ω}) Fn ω \leftrightarrow ({rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) ↾}_{ω}) Fn ω$
5	2 4	mpbir	$⊢ ({Q ↾}_{ω}) Fn ω$
6		fvres	$⊢ b \in ω \to ({Q ↾}_{ω}) (b) = Q (b)$
7	1	seqomlem1	$⊢ b \in ω \to Q (b) = ⟨b, 2^{nd} (Q (b))⟩$
8	6 7	eqtrd	$⊢ b \in ω \to ({Q ↾}_{ω}) (b) = ⟨b, 2^{nd} (Q (b))⟩$
9		fvex	$⊢ 2^{nd} (Q (b)) \in V$
10		opelxpi	$⊢ (b \in ω \land 2^{nd} (Q (b)) \in V) \to ⟨b, 2^{nd} (Q (b))⟩ \in (ω \times V)$
11	9 10	mpan2	$⊢ b \in ω \to ⟨b, 2^{nd} (Q (b))⟩ \in (ω \times V)$
12	8 11	eqeltrd	$⊢ b \in ω \to ({Q ↾}_{ω}) (b) \in (ω \times V)$
13	12	rgen	$⊢ \forall b \in ω ({Q ↾}_{ω}) (b) \in (ω \times V)$
14		ffnfv	$⊢ ({Q ↾}_{ω}) : ω ⟶ ω \times V \leftrightarrow (({Q ↾}_{ω}) Fn ω \land \forall b \in ω ({Q ↾}_{ω}) (b) \in (ω \times V))$
15	5 13 14	mpbir2an	$⊢ ({Q ↾}_{ω}) : ω ⟶ ω \times V$
16		frn	$⊢ ({Q ↾}_{ω}) : ω ⟶ ω \times V \to ran ({Q ↾}_{ω}) \subseteq ω \times V$
17	15 16	ax-mp	$⊢ ran ({Q ↾}_{ω}) \subseteq ω \times V$
18		df-br	$⊢ a ran ({Q ↾}_{ω}) b \leftrightarrow ⟨a, b⟩ \in ran ({Q ↾}_{ω})$
19		fvelrnb	$⊢ ({Q ↾}_{ω}) Fn ω \to (⟨a, b⟩ \in ran ({Q ↾}_{ω}) \leftrightarrow \exists c \in ω ({Q ↾}_{ω}) (c) = ⟨a, b⟩)$
20	5 19	ax-mp	$⊢ ⟨a, b⟩ \in ran ({Q ↾}_{ω}) \leftrightarrow \exists c \in ω ({Q ↾}_{ω}) (c) = ⟨a, b⟩$
21		fvres	$⊢ c \in ω \to ({Q ↾}_{ω}) (c) = Q (c)$
22	21	eqeq1d	$⊢ c \in ω \to (({Q ↾}_{ω}) (c) = ⟨a, b⟩ \leftrightarrow Q (c) = ⟨a, b⟩)$
23	22	rexbiia	$⊢ \exists c \in ω ({Q ↾}_{ω}) (c) = ⟨a, b⟩ \leftrightarrow \exists c \in ω Q (c) = ⟨a, b⟩$
24	18 20 23	3bitri	$⊢ a ran ({Q ↾}_{ω}) b \leftrightarrow \exists c \in ω Q (c) = ⟨a, b⟩$
25	1	seqomlem1	$⊢ c \in ω \to Q (c) = ⟨c, 2^{nd} (Q (c))⟩$
26	25	adantl	$⊢ (a \in ω \land c \in ω) \to Q (c) = ⟨c, 2^{nd} (Q (c))⟩$
27	26	eqeq1d	$⊢ (a \in ω \land c \in ω) \to (Q (c) = ⟨a, b⟩ \leftrightarrow ⟨c, 2^{nd} (Q (c))⟩ = ⟨a, b⟩)$
28		vex	$⊢ c \in V$
29		fvex	$⊢ 2^{nd} (Q (c)) \in V$
30	28 29	opth1	$⊢ ⟨c, 2^{nd} (Q (c))⟩ = ⟨a, b⟩ \to c = a$
31	27 30	syl6bi	$⊢ (a \in ω \land c \in ω) \to (Q (c) = ⟨a, b⟩ \to c = a)$
32		fveqeq2	$⊢ c = a \to (Q (c) = ⟨a, b⟩ \leftrightarrow Q (a) = ⟨a, b⟩)$
33	32	biimpd	$⊢ c = a \to (Q (c) = ⟨a, b⟩ \to Q (a) = ⟨a, b⟩)$
34	31 33	syli	$⊢ (a \in ω \land c \in ω) \to (Q (c) = ⟨a, b⟩ \to Q (a) = ⟨a, b⟩)$
35		fveq2	$⊢ Q (a) = ⟨a, b⟩ \to 2^{nd} (Q (a)) = 2^{nd} (⟨a, b⟩)$
36		vex	$⊢ a \in V$
37		vex	$⊢ b \in V$
38	36 37	op2nd	$⊢ 2^{nd} (⟨a, b⟩) = b$
39	35 38	eqtr2di	$⊢ Q (a) = ⟨a, b⟩ \to b = 2^{nd} (Q (a))$
40	34 39	syl6	$⊢ (a \in ω \land c \in ω) \to (Q (c) = ⟨a, b⟩ \to b = 2^{nd} (Q (a)))$
41	40	rexlimdva	$⊢ a \in ω \to (\exists c \in ω Q (c) = ⟨a, b⟩ \to b = 2^{nd} (Q (a)))$
42	1	seqomlem1	$⊢ a \in ω \to Q (a) = ⟨a, 2^{nd} (Q (a))⟩$
43		fveqeq2	$⊢ c = a \to (Q (c) = ⟨a, 2^{nd} (Q (a))⟩ \leftrightarrow Q (a) = ⟨a, 2^{nd} (Q (a))⟩)$
44	43	rspcev	$⊢ (a \in ω \land Q (a) = ⟨a, 2^{nd} (Q (a))⟩) \to \exists c \in ω Q (c) = ⟨a, 2^{nd} (Q (a))⟩$
45	42 44	mpdan	$⊢ a \in ω \to \exists c \in ω Q (c) = ⟨a, 2^{nd} (Q (a))⟩$
46		opeq2	$⊢ b = 2^{nd} (Q (a)) \to ⟨a, b⟩ = ⟨a, 2^{nd} (Q (a))⟩$
47	46	eqeq2d	$⊢ b = 2^{nd} (Q (a)) \to (Q (c) = ⟨a, b⟩ \leftrightarrow Q (c) = ⟨a, 2^{nd} (Q (a))⟩)$
48	47	rexbidv	$⊢ b = 2^{nd} (Q (a)) \to (\exists c \in ω Q (c) = ⟨a, b⟩ \leftrightarrow \exists c \in ω Q (c) = ⟨a, 2^{nd} (Q (a))⟩)$
49	45 48	syl5ibrcom	$⊢ a \in ω \to (b = 2^{nd} (Q (a)) \to \exists c \in ω Q (c) = ⟨a, b⟩)$
50	41 49	impbid	$⊢ a \in ω \to (\exists c \in ω Q (c) = ⟨a, b⟩ \leftrightarrow b = 2^{nd} (Q (a)))$
51	24 50	bitrid	$⊢ a \in ω \to (a ran ({Q ↾}_{ω}) b \leftrightarrow b = 2^{nd} (Q (a)))$
52	51	alrimiv	$⊢ a \in ω \to \forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = 2^{nd} (Q (a)))$
53		fvex	$⊢ 2^{nd} (Q (a)) \in V$
54		eqeq2	$⊢ c = 2^{nd} (Q (a)) \to (b = c \leftrightarrow b = 2^{nd} (Q (a)))$
55	54	bibi2d	$⊢ c = 2^{nd} (Q (a)) \to ((a ran ({Q ↾}_{ω}) b \leftrightarrow b = c) \leftrightarrow (a ran ({Q ↾}_{ω}) b \leftrightarrow b = 2^{nd} (Q (a))))$
56	55	albidv	$⊢ c = 2^{nd} (Q (a)) \to (\forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = c) \leftrightarrow \forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = 2^{nd} (Q (a))))$
57	53 56	spcev	$⊢ \forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = 2^{nd} (Q (a))) \to \exists c \forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = c)$
58	52 57	syl	$⊢ a \in ω \to \exists c \forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = c)$
59		eu6	$⊢ \exists! b a ran ({Q ↾}_{ω}) b \leftrightarrow \exists c \forall b (a ran ({Q ↾}_{ω}) b \leftrightarrow b = c)$
60	58 59	sylibr	$⊢ a \in ω \to \exists! b a ran ({Q ↾}_{ω}) b$
61	60	rgen	$⊢ \forall a \in ω \exists! b a ran ({Q ↾}_{ω}) b$
62		dff3	$⊢ ran ({Q ↾}_{ω}) : ω ⟶ V \leftrightarrow (ran ({Q ↾}_{ω}) \subseteq ω \times V \land \forall a \in ω \exists! b a ran ({Q ↾}_{ω}) b)$
63	17 61 62	mpbir2an	$⊢ ran ({Q ↾}_{ω}) : ω ⟶ V$
64		df-ima	$⊢ Q [ω] = ran ({Q ↾}_{ω})$
65	64	feq1i	$⊢ Q [ω] : ω ⟶ V \leftrightarrow ran ({Q ↾}_{ω}) : ω ⟶ V$
66	63 65	mpbir	$⊢ Q [ω] : ω ⟶ V$
67		dffn2	$⊢ Q [ω] Fn ω \leftrightarrow Q [ω] : ω ⟶ V$
68	66 67	mpbir	$⊢ Q [ω] Fn ω$

Metamath Proof Explorer

Theorem seqomlem2

Proof