Theorem isf32lem9

Description: Lemma for isfin3-2 . Construction of the onto function. (Contributed by Stefan O'Rear, 5-Nov-2014) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	isf32lem.a	⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
	isf32lem.b	⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
	isf32lem.c	⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
	isf32lem.d	⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) }
	isf32lem.e	⊢ 𝐽 = ( 𝑢 ∈ ω ↦ ( ℩ 𝑣 ∈ 𝑆 ( 𝑣 ∩ 𝑆 ) ≈ 𝑢 ) )
	isf32lem.f	⊢ 𝐾 = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
	isf32lem.g	⊢ 𝐿 = ( 𝑡 ∈ 𝐺 ↦ ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
Assertion	isf32lem9	⊢ ( 𝜑 → 𝐿 : 𝐺 –onto→ ω )

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
2		isf32lem.b	⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
3		isf32lem.c	⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
4		isf32lem.d	⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) }
5		isf32lem.e	⊢ 𝐽 = ( 𝑢 ∈ ω ↦ ( ℩ 𝑣 ∈ 𝑆 ( 𝑣 ∩ 𝑆 ) ≈ 𝑢 ) )
6		isf32lem.f	⊢ 𝐾 = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
7		isf32lem.g	⊢ 𝐿 = ( 𝑡 ∈ 𝐺 ↦ ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
8		ssab2	⊢ { 𝑠 ∣ ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) } ⊆ ω
9		iotacl	⊢ ( ∃! 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ∈ { 𝑠 ∣ ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) } )
10	8 9	sseldi	⊢ ( ∃! 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ∈ ω )
11		iotanul	⊢ ( ¬ ∃! 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) = ∅ )
12		peano1	⊢ ∅ ∈ ω
13	11 12	eqeltrdi	⊢ ( ¬ ∃! 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ∈ ω )
14	10 13	pm2.61i	⊢ ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ∈ ω
15	14	a1i	⊢ ( 𝑡 ∈ 𝐺 → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ∈ ω )
16	7 15	fmpti	⊢ 𝐿 : 𝐺 ⟶ ω
17	16	a1i	⊢ ( 𝜑 → 𝐿 : 𝐺 ⟶ ω )
18	1 2 3 4 5 6	isf32lem6	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ( 𝐾 ‘ 𝑎 ) ≠ ∅ )
19		n0	⊢ ( ( 𝐾 ‘ 𝑎 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) )
20	18 19	sylib	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ∃ 𝑏 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) )
21	1 2 3 4 5 6	isf32lem8	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ( 𝐾 ‘ 𝑎 ) ⊆ 𝐺 )
22	21	sselda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ) ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) → 𝑏 ∈ 𝐺 )
23		eleq1w	⊢ ( 𝑡 = 𝑏 → ( 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ↔ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) )
24	23	anbi2d	⊢ ( 𝑡 = 𝑏 → ( ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ↔ ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
25	24	iotabidv	⊢ ( 𝑡 = 𝑏 → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) = ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
26		iotaex	⊢ ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ∈ V
27	25 7 26	fvmpt3i	⊢ ( 𝑏 ∈ 𝐺 → ( 𝐿 ‘ 𝑏 ) = ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
28	22 27	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ) ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) → ( 𝐿 ‘ 𝑏 ) = ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
29		simp1r	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) )
30		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → 𝜑 )
31		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → 𝑠 ≠ 𝑎 )
32	31	necomd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → 𝑎 ≠ 𝑠 )
33		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → 𝑎 ∈ ω )
34		simpl3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → 𝑠 ∈ ω )
35	1 2 3 4 5 6	isf32lem7	⊢ ( ( ( 𝜑 ∧ 𝑎 ≠ 𝑠 ) ∧ ( 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ) → ( ( 𝐾 ‘ 𝑎 ) ∩ ( 𝐾 ‘ 𝑠 ) ) = ∅ )
36	30 32 33 34 35	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → ( ( 𝐾 ‘ 𝑎 ) ∩ ( 𝐾 ‘ 𝑠 ) ) = ∅ )
37		disj1	⊢ ( ( ( 𝐾 ‘ 𝑎 ) ∩ ( 𝐾 ‘ 𝑠 ) ) = ∅ ↔ ∀ 𝑏 ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) )
38	36 37	sylib	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) ∧ 𝑠 ≠ 𝑎 ) → ∀ 𝑏 ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) )
39	38	ex	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → ( 𝑠 ≠ 𝑎 → ∀ 𝑏 ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
40		sp	⊢ ( ∀ 𝑏 ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) → ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) )
41	39 40	syl6	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → ( 𝑠 ≠ 𝑎 → ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
42	41	com23	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ( 𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
43	42	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ( 𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
44	29 43	mpd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → ( 𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) )
45	44	necon4ad	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω ) → ( 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) → 𝑠 = 𝑎 ) )
46	45	3expia	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ) → ( 𝑠 ∈ ω → ( 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) → 𝑠 = 𝑎 ) ) )
47	46	impd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ) → ( ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) → 𝑠 = 𝑎 ) )
48		eleq1w	⊢ ( 𝑠 = 𝑎 → ( 𝑠 ∈ ω ↔ 𝑎 ∈ ω ) )
49		fveq2	⊢ ( 𝑠 = 𝑎 → ( 𝐾 ‘ 𝑠 ) = ( 𝐾 ‘ 𝑎 ) )
50	49	eleq2d	⊢ ( 𝑠 = 𝑎 → ( 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ↔ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) )
51	48 50	anbi12d	⊢ ( 𝑠 = 𝑎 → ( ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ↔ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ) )
52	51	biimprcd	⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) → ( 𝑠 = 𝑎 → ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
53	52	ancoms	⊢ ( ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ∧ 𝑎 ∈ ω ) → ( 𝑠 = 𝑎 → ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
54	53	adantll	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ) → ( 𝑠 = 𝑎 → ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) )
55	47 54	impbid	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ) → ( ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ↔ 𝑠 = 𝑎 ) )
56	55	iota5	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) ∧ 𝑎 ∈ ω ) → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) = 𝑎 )
57	56	an32s	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ) ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) → ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑠 ) ) ) = 𝑎 )
58	28 57	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ) ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) → 𝑎 = ( 𝐿 ‘ 𝑏 ) )
59	22 58	jca	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ω ) ∧ 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) ) → ( 𝑏 ∈ 𝐺 ∧ 𝑎 = ( 𝐿 ‘ 𝑏 ) ) )
60	59	ex	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ( 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ( 𝑏 ∈ 𝐺 ∧ 𝑎 = ( 𝐿 ‘ 𝑏 ) ) ) )
61	60	eximdv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ( ∃ 𝑏 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ∃ 𝑏 ( 𝑏 ∈ 𝐺 ∧ 𝑎 = ( 𝐿 ‘ 𝑏 ) ) ) )
62		df-rex	⊢ ( ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐿 ‘ 𝑏 ) ↔ ∃ 𝑏 ( 𝑏 ∈ 𝐺 ∧ 𝑎 = ( 𝐿 ‘ 𝑏 ) ) )
63	61 62	syl6ibr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ( ∃ 𝑏 𝑏 ∈ ( 𝐾 ‘ 𝑎 ) → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐿 ‘ 𝑏 ) ) )
64	20 63	mpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ω ) → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐿 ‘ 𝑏 ) )
65	64	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ω ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐿 ‘ 𝑏 ) )
66		dffo3	⊢ ( 𝐿 : 𝐺 –onto→ ω ↔ ( 𝐿 : 𝐺 ⟶ ω ∧ ∀ 𝑎 ∈ ω ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐿 ‘ 𝑏 ) ) )
67	17 65 66	sylanbrc	⊢ ( 𝜑 → 𝐿 : 𝐺 –onto→ ω )