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	$⊢ φ \to F : ω ⟶ 𝒫 G$
	isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
	isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
	isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
	isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
	isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
	isf32lem.g	$⊢ L = (t \in G ⟼ (ι s \| (s \in ω \land t \in K (s))))$
Assertion	isf32lem9	$⊢ φ \to L : G \underset{onto}{⟶} ω$

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
2		isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
3		isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
4		isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
5		isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
6		isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
7		isf32lem.g	$⊢ L = (t \in G ⟼ (ι s \| (s \in ω \land t \in K (s))))$
8		ssab2	$⊢ \{s \| (s \in ω \land t \in K (s))\} \subseteq ω$
9		iotacl	$⊢ \exists! s (s \in ω \land t \in K (s)) \to (ι s \| (s \in ω \land t \in K (s))) \in \{s \| (s \in ω \land t \in K (s))\}$
10	8 9	sseldi	$⊢ \exists! s (s \in ω \land t \in K (s)) \to (ι s \| (s \in ω \land t \in K (s))) \in ω$
11		iotanul	$⊢ \neg \exists! s (s \in ω \land t \in K (s)) \to (ι s \| (s \in ω \land t \in K (s))) = \emptyset$
12		peano1	$⊢ \emptyset \in ω$
13	11 12	eqeltrdi	$⊢ \neg \exists! s (s \in ω \land t \in K (s)) \to (ι s \| (s \in ω \land t \in K (s))) \in ω$
14	10 13	pm2.61i	$⊢ (ι s \| (s \in ω \land t \in K (s))) \in ω$
15	14	a1i	$⊢ t \in G \to (ι s \| (s \in ω \land t \in K (s))) \in ω$
16	7 15	fmpti	$⊢ L : G ⟶ ω$
17	16	a1i	$⊢ φ \to L : G ⟶ ω$
18	1 2 3 4 5 6	isf32lem6	$⊢ (φ \land a \in ω) \to K (a) \neq \emptyset$
19		n0	$⊢ K (a) \neq \emptyset \leftrightarrow \exists b b \in K (a)$
20	18 19	sylib	$⊢ (φ \land a \in ω) \to \exists b b \in K (a)$
21	1 2 3 4 5 6	isf32lem8	$⊢ (φ \land a \in ω) \to K (a) \subseteq G$
22	21	sselda	$⊢ ((φ \land a \in ω) \land b \in K (a)) \to b \in G$
23		eleq1w	$⊢ t = b \to (t \in K (s) \leftrightarrow b \in K (s))$
24	23	anbi2d	$⊢ t = b \to ((s \in ω \land t \in K (s)) \leftrightarrow (s \in ω \land b \in K (s)))$
25	24	iotabidv	$⊢ t = b \to (ι s \| (s \in ω \land t \in K (s))) = (ι s \| (s \in ω \land b \in K (s)))$
26		iotaex	$⊢ (ι s \| (s \in ω \land t \in K (s))) \in V$
27	25 7 26	fvmpt3i	$⊢ b \in G \to L (b) = (ι s \| (s \in ω \land b \in K (s)))$
28	22 27	syl	$⊢ ((φ \land a \in ω) \land b \in K (a)) \to L (b) = (ι s \| (s \in ω \land b \in K (s)))$
29		simp1r	$⊢ ((φ \land b \in K (a)) \land a \in ω \land s \in ω) \to b \in K (a)$
30		simpl1	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to φ$
31		simpr	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to s \neq a$
32	31	necomd	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to a \neq s$
33		simpl2	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to a \in ω$
34		simpl3	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to s \in ω$
35	1 2 3 4 5 6	isf32lem7	$⊢ ((φ \land a \neq s) \land (a \in ω \land s \in ω)) \to K (a) \cap K (s) = \emptyset$
36	30 32 33 34 35	syl22anc	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to K (a) \cap K (s) = \emptyset$
37		disj1	$⊢ K (a) \cap K (s) = \emptyset \leftrightarrow \forall b (b \in K (a) \to \neg b \in K (s))$
38	36 37	sylib	$⊢ ((φ \land a \in ω \land s \in ω) \land s \neq a) \to \forall b (b \in K (a) \to \neg b \in K (s))$
39	38	ex	$⊢ (φ \land a \in ω \land s \in ω) \to (s \neq a \to \forall b (b \in K (a) \to \neg b \in K (s)))$
40		sp	$⊢ \forall b (b \in K (a) \to \neg b \in K (s)) \to (b \in K (a) \to \neg b \in K (s))$
41	39 40	syl6	$⊢ (φ \land a \in ω \land s \in ω) \to (s \neq a \to (b \in K (a) \to \neg b \in K (s)))$
42	41	com23	$⊢ (φ \land a \in ω \land s \in ω) \to (b \in K (a) \to (s \neq a \to \neg b \in K (s)))$
43	42	3adant1r	$⊢ ((φ \land b \in K (a)) \land a \in ω \land s \in ω) \to (b \in K (a) \to (s \neq a \to \neg b \in K (s)))$
44	29 43	mpd	$⊢ ((φ \land b \in K (a)) \land a \in ω \land s \in ω) \to (s \neq a \to \neg b \in K (s))$
45	44	necon4ad	$⊢ ((φ \land b \in K (a)) \land a \in ω \land s \in ω) \to (b \in K (s) \to s = a)$
46	45	3expia	$⊢ ((φ \land b \in K (a)) \land a \in ω) \to (s \in ω \to (b \in K (s) \to s = a))$
47	46	impd	$⊢ ((φ \land b \in K (a)) \land a \in ω) \to ((s \in ω \land b \in K (s)) \to s = a)$
48		eleq1w	$⊢ s = a \to (s \in ω \leftrightarrow a \in ω)$
49		fveq2	$⊢ s = a \to K (s) = K (a)$
50	49	eleq2d	$⊢ s = a \to (b \in K (s) \leftrightarrow b \in K (a))$
51	48 50	anbi12d	$⊢ s = a \to ((s \in ω \land b \in K (s)) \leftrightarrow (a \in ω \land b \in K (a)))$
52	51	biimprcd	$⊢ (a \in ω \land b \in K (a)) \to (s = a \to (s \in ω \land b \in K (s)))$
53	52	ancoms	$⊢ (b \in K (a) \land a \in ω) \to (s = a \to (s \in ω \land b \in K (s)))$
54	53	adantll	$⊢ ((φ \land b \in K (a)) \land a \in ω) \to (s = a \to (s \in ω \land b \in K (s)))$
55	47 54	impbid	$⊢ ((φ \land b \in K (a)) \land a \in ω) \to ((s \in ω \land b \in K (s)) \leftrightarrow s = a)$
56	55	iota5	$⊢ ((φ \land b \in K (a)) \land a \in ω) \to (ι s \| (s \in ω \land b \in K (s))) = a$
57	56	an32s	$⊢ ((φ \land a \in ω) \land b \in K (a)) \to (ι s \| (s \in ω \land b \in K (s))) = a$
58	28 57	eqtr2d	$⊢ ((φ \land a \in ω) \land b \in K (a)) \to a = L (b)$
59	22 58	jca	$⊢ ((φ \land a \in ω) \land b \in K (a)) \to (b \in G \land a = L (b))$
60	59	ex	$⊢ (φ \land a \in ω) \to (b \in K (a) \to (b \in G \land a = L (b)))$
61	60	eximdv	$⊢ (φ \land a \in ω) \to (\exists b b \in K (a) \to \exists b (b \in G \land a = L (b)))$
62		df-rex	$⊢ \exists b \in G a = L (b) \leftrightarrow \exists b (b \in G \land a = L (b))$
63	61 62	syl6ibr	$⊢ (φ \land a \in ω) \to (\exists b b \in K (a) \to \exists b \in G a = L (b))$
64	20 63	mpd	$⊢ (φ \land a \in ω) \to \exists b \in G a = L (b)$
65	64	ralrimiva	$⊢ φ \to \forall a \in ω \exists b \in G a = L (b)$
66		dffo3	$⊢ L : G \underset{onto}{⟶} ω \leftrightarrow (L : G ⟶ ω \land \forall a \in ω \exists b \in G a = L (b))$
67	17 65 66	sylanbrc	$⊢ φ \to L : G \underset{onto}{⟶} ω$

Metamath Proof Explorer

Theorem isf32lem9

Proof