unbenlem

Description: Lemma for unben . (Contributed by NM, 5-May-2005) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Hypothesis	unbenlem.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}$
	Assertion	unbenlem	$⊢ (A \subseteq ℕ \land \forall m \in ℕ \exists n \in A m < n) \to A \approx ω$

Proof

Step	Hyp	Ref	Expression
1		unbenlem.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}$
2		nnex	$⊢ ℕ \in V$
3	2	ssex	$⊢ A \subseteq ℕ \to A \in V$
4		1z	$⊢ 1 \in ℤ$
5	4 1	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 1}$
6		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
7		f1oeq3	$⊢ ℕ = ℤ_{\geq 1} \to (G : ω \underset{1-1 onto}{⟶} ℕ \leftrightarrow G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 1})$
8	6 7	ax-mp	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ \leftrightarrow G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 1}$
9	5 8	mpbir	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ$
10		f1ocnv	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ \to G^{-1} : ℕ \underset{1-1 onto}{⟶} ω$
11		f1of1	$⊢ G^{-1} : ℕ \underset{1-1 onto}{⟶} ω \to G^{-1} : ℕ \underset{1-1}{⟶} ω$
12	9 10 11	mp2b	$⊢ G^{-1} : ℕ \underset{1-1}{⟶} ω$
13		f1ores	$⊢ (G^{-1} : ℕ \underset{1-1}{⟶} ω \land A \subseteq ℕ) \to ({G^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} G^{-1} [A]$
14	12 13	mpan	$⊢ A \subseteq ℕ \to ({G^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} G^{-1} [A]$
15		f1oeng	$⊢ (A \in V \land ({G^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} G^{-1} [A]) \to A \approx G^{-1} [A]$
16	3 14 15	syl2anc	$⊢ A \subseteq ℕ \to A \approx G^{-1} [A]$
17	16	adantr	$⊢ (A \subseteq ℕ \land \forall m \in ℕ \exists n \in A m < n) \to A \approx G^{-1} [A]$
18		imassrn	$⊢ G^{-1} [A] \subseteq ran G^{-1}$
19		dfdm4	$⊢ dom G = ran G^{-1}$
20		f1of	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ \to G : ω ⟶ ℕ$
21	9 20	ax-mp	$⊢ G : ω ⟶ ℕ$
22	21	fdmi	$⊢ dom G = ω$
23	19 22	eqtr3i	$⊢ ran G^{-1} = ω$
24	18 23	sseqtri	$⊢ G^{-1} [A] \subseteq ω$
25	4 1	om2uzuzi	$⊢ y \in ω \to G (y) \in ℤ_{\geq 1}$
26	25 6	eleqtrrdi	$⊢ y \in ω \to G (y) \in ℕ$
27		breq1	$⊢ m = G (y) \to (m < n \leftrightarrow G (y) < n)$
28	27	rexbidv	$⊢ m = G (y) \to (\exists n \in A m < n \leftrightarrow \exists n \in A G (y) < n)$
29	28	rspcv	$⊢ G (y) \in ℕ \to (\forall m \in ℕ \exists n \in A m < n \to \exists n \in A G (y) < n)$
30	26 29	syl	$⊢ y \in ω \to (\forall m \in ℕ \exists n \in A m < n \to \exists n \in A G (y) < n)$
31	30	adantr	$⊢ (y \in ω \land A \subseteq ℕ) \to (\forall m \in ℕ \exists n \in A m < n \to \exists n \in A G (y) < n)$
32		f1ocnv	$⊢ ({G^{-1} ↾}_{A}) : A \underset{1-1 onto}{⟶} G^{-1} [A] \to {({G^{-1} ↾}_{A})}^{-1} : G^{-1} [A] \underset{1-1 onto}{⟶} A$
33	14 32	syl	$⊢ A \subseteq ℕ \to {({G^{-1} ↾}_{A})}^{-1} : G^{-1} [A] \underset{1-1 onto}{⟶} A$
34		f1ofun	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ \to Fun G$
35	9 34	ax-mp	$⊢ Fun G$
36		funcnvres2	$⊢ Fun G \to {({G^{-1} ↾}_{A})}^{-1} = {G ↾}_{G^{-1} [A]}$
37		f1oeq1	$⊢ {({G^{-1} ↾}_{A})}^{-1} = {G ↾}_{G^{-1} [A]} \to ({({G^{-1} ↾}_{A})}^{-1} : G^{-1} [A] \underset{1-1 onto}{⟶} A \leftrightarrow ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A)$
38	35 36 37	mp2b	$⊢ {({G^{-1} ↾}_{A})}^{-1} : G^{-1} [A] \underset{1-1 onto}{⟶} A \leftrightarrow ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A$
39	33 38	sylib	$⊢ A \subseteq ℕ \to ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A$
40		f1ofo	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A \to ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{onto}{⟶} A$
41		forn	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{onto}{⟶} A \to ran ({G ↾}_{G^{-1} [A]}) = A$
42	40 41	syl	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A \to ran ({G ↾}_{G^{-1} [A]}) = A$
43	42	eleq2d	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A \to (n \in ran ({G ↾}_{G^{-1} [A]}) \leftrightarrow n \in A)$
44		f1ofn	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A \to ({G ↾}_{G^{-1} [A]}) Fn G^{-1} [A]$
45		fvelrnb	$⊢ ({G ↾}_{G^{-1} [A]}) Fn G^{-1} [A] \to (n \in ran ({G ↾}_{G^{-1} [A]}) \leftrightarrow \exists m \in G^{-1} [A] ({G ↾}_{G^{-1} [A]}) (m) = n)$
46	44 45	syl	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A \to (n \in ran ({G ↾}_{G^{-1} [A]}) \leftrightarrow \exists m \in G^{-1} [A] ({G ↾}_{G^{-1} [A]}) (m) = n)$
47	43 46	bitr3d	$⊢ ({G ↾}_{G^{-1} [A]}) : G^{-1} [A] \underset{1-1 onto}{⟶} A \to (n \in A \leftrightarrow \exists m \in G^{-1} [A] ({G ↾}_{G^{-1} [A]}) (m) = n)$
48	39 47	syl	$⊢ A \subseteq ℕ \to (n \in A \leftrightarrow \exists m \in G^{-1} [A] ({G ↾}_{G^{-1} [A]}) (m) = n)$
49	48	biimpa	$⊢ (A \subseteq ℕ \land n \in A) \to \exists m \in G^{-1} [A] ({G ↾}_{G^{-1} [A]}) (m) = n$
50		fvres	$⊢ m \in G^{-1} [A] \to ({G ↾}_{G^{-1} [A]}) (m) = G (m)$
51	50	eqeq1d	$⊢ m \in G^{-1} [A] \to (({G ↾}_{G^{-1} [A]}) (m) = n \leftrightarrow G (m) = n)$
52	51	biimpa	$⊢ (m \in G^{-1} [A] \land ({G ↾}_{G^{-1} [A]}) (m) = n) \to G (m) = n$
53	52	adantll	$⊢ ((y \in ω \land m \in G^{-1} [A]) \land ({G ↾}_{G^{-1} [A]}) (m) = n) \to G (m) = n$
54	24	sseli	$⊢ m \in G^{-1} [A] \to m \in ω$
55	4 1	om2uzlt2i	$⊢ (y \in ω \land m \in ω) \to (y \in m \leftrightarrow G (y) < G (m))$
56	54 55	sylan2	$⊢ (y \in ω \land m \in G^{-1} [A]) \to (y \in m \leftrightarrow G (y) < G (m))$
57		breq2	$⊢ G (m) = n \to (G (y) < G (m) \leftrightarrow G (y) < n)$
58	56 57	sylan9bb	$⊢ ((y \in ω \land m \in G^{-1} [A]) \land G (m) = n) \to (y \in m \leftrightarrow G (y) < n)$
59	53 58	syldan	$⊢ ((y \in ω \land m \in G^{-1} [A]) \land ({G ↾}_{G^{-1} [A]}) (m) = n) \to (y \in m \leftrightarrow G (y) < n)$
60	59	biimparc	$⊢ (G (y) < n \land ((y \in ω \land m \in G^{-1} [A]) \land ({G ↾}_{G^{-1} [A]}) (m) = n)) \to y \in m$
61	60	exp44	$⊢ G (y) < n \to (y \in ω \to (m \in G^{-1} [A] \to (({G ↾}_{G^{-1} [A]}) (m) = n \to y \in m)))$
62	61	imp31	$⊢ ((G (y) < n \land y \in ω) \land m \in G^{-1} [A]) \to (({G ↾}_{G^{-1} [A]}) (m) = n \to y \in m)$
63	62	reximdva	$⊢ (G (y) < n \land y \in ω) \to (\exists m \in G^{-1} [A] ({G ↾}_{G^{-1} [A]}) (m) = n \to \exists m \in G^{-1} [A] y \in m)$
64	49 63	syl5	$⊢ (G (y) < n \land y \in ω) \to ((A \subseteq ℕ \land n \in A) \to \exists m \in G^{-1} [A] y \in m)$
65	64	exp4b	$⊢ G (y) < n \to (y \in ω \to (A \subseteq ℕ \to (n \in A \to \exists m \in G^{-1} [A] y \in m)))$
66	65	com4l	$⊢ y \in ω \to (A \subseteq ℕ \to (n \in A \to (G (y) < n \to \exists m \in G^{-1} [A] y \in m)))$
67	66	imp	$⊢ (y \in ω \land A \subseteq ℕ) \to (n \in A \to (G (y) < n \to \exists m \in G^{-1} [A] y \in m))$
68	67	rexlimdv	$⊢ (y \in ω \land A \subseteq ℕ) \to (\exists n \in A G (y) < n \to \exists m \in G^{-1} [A] y \in m)$
69	31 68	syld	$⊢ (y \in ω \land A \subseteq ℕ) \to (\forall m \in ℕ \exists n \in A m < n \to \exists m \in G^{-1} [A] y \in m)$
70	69	ex	$⊢ y \in ω \to (A \subseteq ℕ \to (\forall m \in ℕ \exists n \in A m < n \to \exists m \in G^{-1} [A] y \in m))$
71	70	com3l	$⊢ A \subseteq ℕ \to (\forall m \in ℕ \exists n \in A m < n \to (y \in ω \to \exists m \in G^{-1} [A] y \in m))$
72	71	imp	$⊢ (A \subseteq ℕ \land \forall m \in ℕ \exists n \in A m < n) \to (y \in ω \to \exists m \in G^{-1} [A] y \in m)$
73	72	ralrimiv	$⊢ (A \subseteq ℕ \land \forall m \in ℕ \exists n \in A m < n) \to \forall y \in ω \exists m \in G^{-1} [A] y \in m$
74		unbnn3	$⊢ (G^{-1} [A] \subseteq ω \land \forall y \in ω \exists m \in G^{-1} [A] y \in m) \to G^{-1} [A] \approx ω$
75	24 73 74	sylancr	$⊢ (A \subseteq ℕ \land \forall m \in ℕ \exists n \in A m < n) \to G^{-1} [A] \approx ω$
76		entr	$⊢ (A \approx G^{-1} [A] \land G^{-1} [A] \approx ω) \to A \approx ω$
77	17 75 76	syl2anc	$⊢ (A \subseteq ℕ \land \forall m \in ℕ \exists n \in A m < n) \to A \approx ω$

Metamath Proof Explorer

Theorem unbenlem

Proof