Theorem 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	⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
Assertion	seqomlem2	⊢ ( 𝑄 “ ω ) Fn ω

Proof

Step	Hyp	Ref	Expression
1		seqomlem.a	⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
2		frfnom	⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) Fn ω
3	1	reseq1i	⊢ ( 𝑄 ↾ ω ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω )
4	3	fneq1i	⊢ ( ( 𝑄 ↾ ω ) Fn ω ↔ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) Fn ω )
5	2 4	mpbir	⊢ ( 𝑄 ↾ ω ) Fn ω
6		fvres	⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) )
7	1	seqomlem1	⊢ ( 𝑏 ∈ ω → ( 𝑄 ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ )
8	6 7	eqtrd	⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ )
9		fvex	⊢ ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ∈ V
10		opelxpi	⊢ ( ( 𝑏 ∈ ω ∧ ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ∈ V ) → ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ ∈ ( ω × V ) )
11	9 10	mpan2	⊢ ( 𝑏 ∈ ω → ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ ∈ ( ω × V ) )
12	8 11	eqeltrd	⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝑏 ) ∈ ( ω × V ) )
13	12	rgen	⊢ ∀ 𝑏 ∈ ω ( ( 𝑄 ↾ ω ) ‘ 𝑏 ) ∈ ( ω × V )
14		ffnfv	⊢ ( ( 𝑄 ↾ ω ) : ω ⟶ ( ω × V ) ↔ ( ( 𝑄 ↾ ω ) Fn ω ∧ ∀ 𝑏 ∈ ω ( ( 𝑄 ↾ ω ) ‘ 𝑏 ) ∈ ( ω × V ) ) )
15	5 13 14	mpbir2an	⊢ ( 𝑄 ↾ ω ) : ω ⟶ ( ω × V )
16		frn	⊢ ( ( 𝑄 ↾ ω ) : ω ⟶ ( ω × V ) → ran ( 𝑄 ↾ ω ) ⊆ ( ω × V ) )
17	15 16	ax-mp	⊢ ran ( 𝑄 ↾ ω ) ⊆ ( ω × V )
18		df-br	⊢ ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ran ( 𝑄 ↾ ω ) )
19		fvelrnb	⊢ ( ( 𝑄 ↾ ω ) Fn ω → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ran ( 𝑄 ↾ ω ) ↔ ∃ 𝑐 ∈ ω ( ( 𝑄 ↾ ω ) ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
20	5 19	ax-mp	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ran ( 𝑄 ↾ ω ) ↔ ∃ 𝑐 ∈ ω ( ( 𝑄 ↾ ω ) ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ )
21		fvres	⊢ ( 𝑐 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) )
22	21	eqeq1d	⊢ ( 𝑐 ∈ ω → ( ( ( 𝑄 ↾ ω ) ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
23	22	rexbiia	⊢ ( ∃ 𝑐 ∈ ω ( ( 𝑄 ↾ ω ) ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ )
24	18 20 23	3bitri	⊢ ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ )
25	1	seqomlem1	⊢ ( 𝑐 ∈ ω → ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑐 , ( 2nd ‘ ( 𝑄 ‘ 𝑐 ) ) ⟩ )
26	25	adantl	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ω ) → ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑐 , ( 2nd ‘ ( 𝑄 ‘ 𝑐 ) ) ⟩ )
27	26	eqeq1d	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ω ) → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑐 , ( 2nd ‘ ( 𝑄 ‘ 𝑐 ) ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
28		vex	⊢ 𝑐 ∈ V
29		fvex	⊢ ( 2nd ‘ ( 𝑄 ‘ 𝑐 ) ) ∈ V
30	28 29	opth1	⊢ ( ⟨ 𝑐 , ( 2nd ‘ ( 𝑄 ‘ 𝑐 ) ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → 𝑐 = 𝑎 )
31	27 30	syl6bi	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ω ) → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ → 𝑐 = 𝑎 ) )
32		fveqeq2	⊢ ( 𝑐 = 𝑎 → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
33	32	biimpd	⊢ ( 𝑐 = 𝑎 → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
34	31 33	syli	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ω ) → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
35		fveq2	⊢ ( ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) = ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
36		vex	⊢ 𝑎 ∈ V
37		vex	⊢ 𝑏 ∈ V
38	36 37	op2nd	⊢ ( 2nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑏
39	35 38	eqtr2di	⊢ ( ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , 𝑏 ⟩ → 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) )
40	34 39	syl6	⊢ ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ω ) → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ → 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) )
41	40	rexlimdva	⊢ ( 𝑎 ∈ ω → ( ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ → 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) )
42	1	seqomlem1	⊢ ( 𝑎 ∈ ω → ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ )
43		fveqeq2	⊢ ( 𝑐 = 𝑎 → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ↔ ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ) )
44	43	rspcev	⊢ ( ( 𝑎 ∈ ω ∧ ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ )
45	42 44	mpdan	⊢ ( 𝑎 ∈ ω → ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ )
46		opeq2	⊢ ( 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ )
47	46	eqeq2d	⊢ ( 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ( ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ) )
48	47	rexbidv	⊢ ( 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ( ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ) )
49	45 48	syl5ibrcom	⊢ ( 𝑎 ∈ ω → ( 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
50	41 49	impbid	⊢ ( 𝑎 ∈ ω → ( ∃ 𝑐 ∈ ω ( 𝑄 ‘ 𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) )
51	24 50	syl5bb	⊢ ( 𝑎 ∈ ω → ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) )
52	51	alrimiv	⊢ ( 𝑎 ∈ ω → ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) )
53		fvex	⊢ ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ∈ V
54		eqeq2	⊢ ( 𝑐 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ( 𝑏 = 𝑐 ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) )
55	54	bibi2d	⊢ ( 𝑐 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ( ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = 𝑐 ) ↔ ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) ) )
56	55	albidv	⊢ ( 𝑐 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) → ( ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = 𝑐 ) ↔ ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) ) )
57	53 56	spcev	⊢ ( ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ) → ∃ 𝑐 ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = 𝑐 ) )
58	52 57	syl	⊢ ( 𝑎 ∈ ω → ∃ 𝑐 ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = 𝑐 ) )
59		eu6	⊢ ( ∃! 𝑏 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ ∃ 𝑐 ∀ 𝑏 ( 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ↔ 𝑏 = 𝑐 ) )
60	58 59	sylibr	⊢ ( 𝑎 ∈ ω → ∃! 𝑏 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 )
61	60	rgen	⊢ ∀ 𝑎 ∈ ω ∃! 𝑏 𝑎 ran ( 𝑄 ↾ ω ) 𝑏
62		dff3	⊢ ( ran ( 𝑄 ↾ ω ) : ω ⟶ V ↔ ( ran ( 𝑄 ↾ ω ) ⊆ ( ω × V ) ∧ ∀ 𝑎 ∈ ω ∃! 𝑏 𝑎 ran ( 𝑄 ↾ ω ) 𝑏 ) )
63	17 61 62	mpbir2an	⊢ ran ( 𝑄 ↾ ω ) : ω ⟶ V
64		df-ima	⊢ ( 𝑄 “ ω ) = ran ( 𝑄 ↾ ω )
65	64	feq1i	⊢ ( ( 𝑄 “ ω ) : ω ⟶ V ↔ ran ( 𝑄 ↾ ω ) : ω ⟶ V )
66	63 65	mpbir	⊢ ( 𝑄 “ ω ) : ω ⟶ V
67		dffn2	⊢ ( ( 𝑄 “ ω ) Fn ω ↔ ( 𝑄 “ ω ) : ω ⟶ V )
68	66 67	mpbir	⊢ ( 𝑄 “ ω ) Fn ω