inf3lem6

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-Oct-1996)

	Ref	Expression
Hypotheses	inf3lem.1	$⊢ G = (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\})$
	inf3lem.2	$⊢ F = {rec (G, \emptyset) ↾}_{ω}$
	inf3lem.3	$⊢ A \in V$
	inf3lem.4	$⊢ B \in V$
Assertion	inf3lem6	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to F : ω \underset{1-1}{⟶} 𝒫 x$

Proof

Step	Hyp	Ref	Expression
1		inf3lem.1	$⊢ G = (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\})$
2		inf3lem.2	$⊢ F = {rec (G, \emptyset) ↾}_{ω}$
3		inf3lem.3	$⊢ A \in V$
4		inf3lem.4	$⊢ B \in V$
5		vex	$⊢ u \in V$
6		vex	$⊢ v \in V$
7	1 2 5 6	inf3lem5	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ((u \in ω \land v \in u) \to F (v) \subset F (u))$
8		dfpss2	$⊢ F (v) \subset F (u) \leftrightarrow (F (v) \subseteq F (u) \land \neg F (v) = F (u))$
9	8	simprbi	$⊢ F (v) \subset F (u) \to \neg F (v) = F (u)$
10	7 9	syl6	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ((u \in ω \land v \in u) \to \neg F (v) = F (u))$
11	10	expdimp	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land u \in ω) \to (v \in u \to \neg F (v) = F (u))$
12	11	adantrl	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land (v \in ω \land u \in ω)) \to (v \in u \to \neg F (v) = F (u))$
13	1 2 6 5	inf3lem5	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ((v \in ω \land u \in v) \to F (u) \subset F (v))$
14		dfpss2	$⊢ F (u) \subset F (v) \leftrightarrow (F (u) \subseteq F (v) \land \neg F (u) = F (v))$
15	14	simprbi	$⊢ F (u) \subset F (v) \to \neg F (u) = F (v)$
16		eqcom	$⊢ F (u) = F (v) \leftrightarrow F (v) = F (u)$
17	15 16	sylnib	$⊢ F (u) \subset F (v) \to \neg F (v) = F (u)$
18	13 17	syl6	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ((v \in ω \land u \in v) \to \neg F (v) = F (u))$
19	18	expdimp	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land v \in ω) \to (u \in v \to \neg F (v) = F (u))$
20	19	adantrr	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land (v \in ω \land u \in ω)) \to (u \in v \to \neg F (v) = F (u))$
21	12 20	jaod	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land (v \in ω \land u \in ω)) \to ((v \in u \lor u \in v) \to \neg F (v) = F (u))$
22	21	con2d	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land (v \in ω \land u \in ω)) \to (F (v) = F (u) \to \neg (v \in u \lor u \in v))$
23		nnord	$⊢ v \in ω \to Ord v$
24		nnord	$⊢ u \in ω \to Ord u$
25		ordtri3	$⊢ (Ord v \land Ord u) \to (v = u \leftrightarrow \neg (v \in u \lor u \in v))$
26	23 24 25	syl2an	$⊢ (v \in ω \land u \in ω) \to (v = u \leftrightarrow \neg (v \in u \lor u \in v))$
27	26	adantl	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land (v \in ω \land u \in ω)) \to (v = u \leftrightarrow \neg (v \in u \lor u \in v))$
28	22 27	sylibrd	$⊢ ((x \neq \emptyset \land x \subseteq ⋃ x) \land (v \in ω \land u \in ω)) \to (F (v) = F (u) \to v = u)$
29	28	ralrimivva	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to \forall v \in ω \forall u \in ω (F (v) = F (u) \to v = u)$
30		frfnom	$⊢ ({rec (G, \emptyset) ↾}_{ω}) Fn ω$
31		fneq1	$⊢ F = {rec (G, \emptyset) ↾}_{ω} \to (F Fn ω \leftrightarrow ({rec (G, \emptyset) ↾}_{ω}) Fn ω)$
32	30 31	mpbiri	$⊢ F = {rec (G, \emptyset) ↾}_{ω} \to F Fn ω$
33		fvelrnb	$⊢ F Fn ω \to (u \in ran F \leftrightarrow \exists v \in ω F (v) = u)$
34	1 2 6 4	inf3lemd	$⊢ v \in ω \to F (v) \subseteq x$
35		fvex	$⊢ F (v) \in V$
36	35	elpw	$⊢ F (v) \in 𝒫 x \leftrightarrow F (v) \subseteq x$
37	34 36	sylibr	$⊢ v \in ω \to F (v) \in 𝒫 x$
38		eleq1	$⊢ F (v) = u \to (F (v) \in 𝒫 x \leftrightarrow u \in 𝒫 x)$
39	37 38	syl5ibcom	$⊢ v \in ω \to (F (v) = u \to u \in 𝒫 x)$
40	39	rexlimiv	$⊢ \exists v \in ω F (v) = u \to u \in 𝒫 x$
41	33 40	syl6bi	$⊢ F Fn ω \to (u \in ran F \to u \in 𝒫 x)$
42	41	ssrdv	$⊢ F Fn ω \to ran F \subseteq 𝒫 x$
43	42	ancli	$⊢ F Fn ω \to (F Fn ω \land ran F \subseteq 𝒫 x)$
44	2 32 43	mp2b	$⊢ (F Fn ω \land ran F \subseteq 𝒫 x)$
45		df-f	$⊢ F : ω ⟶ 𝒫 x \leftrightarrow (F Fn ω \land ran F \subseteq 𝒫 x)$
46	44 45	mpbir	$⊢ F : ω ⟶ 𝒫 x$
47	29 46	jctil	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to (F : ω ⟶ 𝒫 x \land \forall v \in ω \forall u \in ω (F (v) = F (u) \to v = u))$
48		dff13	$⊢ F : ω \underset{1-1}{⟶} 𝒫 x \leftrightarrow (F : ω ⟶ 𝒫 x \land \forall v \in ω \forall u \in ω (F (v) = F (u) \to v = u))$
49	47 48	sylibr	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to F : ω \underset{1-1}{⟶} 𝒫 x$

Metamath Proof Explorer

Theorem inf3lem6

Proof