inf3lem2

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-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	inf3lem2	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to (A \in ω \to F (A) \neq 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		fveq2	$⊢ v = \emptyset \to F (v) = F (\emptyset)$
6	5	neeq1d	$⊢ v = \emptyset \to (F (v) \neq x \leftrightarrow F (\emptyset) \neq x)$
7	6	imbi2d	$⊢ v = \emptyset \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (v) \neq x) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (\emptyset) \neq x))$
8		fveq2	$⊢ v = u \to F (v) = F (u)$
9	8	neeq1d	$⊢ v = u \to (F (v) \neq x \leftrightarrow F (u) \neq x)$
10	9	imbi2d	$⊢ v = u \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (v) \neq x) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (u) \neq x))$
11		fveq2	$⊢ v = suc u \to F (v) = F (suc u)$
12	11	neeq1d	$⊢ v = suc u \to (F (v) \neq x \leftrightarrow F (suc u) \neq x)$
13	12	imbi2d	$⊢ v = suc u \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (v) \neq x) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (suc u) \neq x))$
14		fveq2	$⊢ v = A \to F (v) = F (A)$
15	14	neeq1d	$⊢ v = A \to (F (v) \neq x \leftrightarrow F (A) \neq x)$
16	15	imbi2d	$⊢ v = A \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (v) \neq x) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (A) \neq x))$
17	1 2 3 4	inf3lemb	$⊢ F (\emptyset) = \emptyset$
18	17	eqeq1i	$⊢ F (\emptyset) = x \leftrightarrow \emptyset = x$
19		eqcom	$⊢ \emptyset = x \leftrightarrow x = \emptyset$
20	18 19	sylbb	$⊢ F (\emptyset) = x \to x = \emptyset$
21	20	necon3i	$⊢ x \neq \emptyset \to F (\emptyset) \neq x$
22	21	adantr	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to F (\emptyset) \neq x$
23		vex	$⊢ u \in V$
24	1 2 23 4	inf3lemd	$⊢ u \in ω \to F (u) \subseteq x$
25		df-pss	$⊢ F (u) \subset x \leftrightarrow (F (u) \subseteq x \land F (u) \neq x)$
26		pssnel	$⊢ F (u) \subset x \to \exists v (v \in x \land \neg v \in F (u))$
27	25 26	sylbir	$⊢ (F (u) \subseteq x \land F (u) \neq x) \to \exists v (v \in x \land \neg v \in F (u))$
28		ssel	$⊢ x \subseteq ⋃ x \to (v \in x \to v \in ⋃ x)$
29		eluni	$⊢ v \in ⋃ x \leftrightarrow \exists f (v \in f \land f \in x)$
30	28 29	syl6ib	$⊢ x \subseteq ⋃ x \to (v \in x \to \exists f (v \in f \land f \in x))$
31		eleq2	$⊢ F (suc u) = x \to (f \in F (suc u) \leftrightarrow f \in x)$
32	31	biimparc	$⊢ (f \in x \land F (suc u) = x) \to f \in F (suc u)$
33	1 2 23 4	inf3lemc	$⊢ u \in ω \to F (suc u) = G (F (u))$
34	33	eleq2d	$⊢ u \in ω \to (f \in F (suc u) \leftrightarrow f \in G (F (u)))$
35		elin	$⊢ v \in (f \cap x) \leftrightarrow (v \in f \land v \in x)$
36		vex	$⊢ f \in V$
37		fvex	$⊢ F (u) \in V$
38	1 2 36 37	inf3lema	$⊢ f \in G (F (u)) \leftrightarrow (f \in x \land f \cap x \subseteq F (u))$
39	38	simprbi	$⊢ f \in G (F (u)) \to f \cap x \subseteq F (u)$
40	39	sseld	$⊢ f \in G (F (u)) \to (v \in (f \cap x) \to v \in F (u))$
41	35 40	syl5bir	$⊢ f \in G (F (u)) \to ((v \in f \land v \in x) \to v \in F (u))$
42	34 41	syl6bi	$⊢ u \in ω \to (f \in F (suc u) \to ((v \in f \land v \in x) \to v \in F (u)))$
43	32 42	syl5	$⊢ u \in ω \to ((f \in x \land F (suc u) = x) \to ((v \in f \land v \in x) \to v \in F (u)))$
44	43	com23	$⊢ u \in ω \to ((v \in f \land v \in x) \to ((f \in x \land F (suc u) = x) \to v \in F (u)))$
45	44	exp5c	$⊢ u \in ω \to (v \in f \to (v \in x \to (f \in x \to (F (suc u) = x \to v \in F (u)))))$
46	45	com34	$⊢ u \in ω \to (v \in f \to (f \in x \to (v \in x \to (F (suc u) = x \to v \in F (u)))))$
47	46	impd	$⊢ u \in ω \to ((v \in f \land f \in x) \to (v \in x \to (F (suc u) = x \to v \in F (u))))$
48	47	exlimdv	$⊢ u \in ω \to (\exists f (v \in f \land f \in x) \to (v \in x \to (F (suc u) = x \to v \in F (u))))$
49	30 48	sylan9r	$⊢ (u \in ω \land x \subseteq ⋃ x) \to (v \in x \to (v \in x \to (F (suc u) = x \to v \in F (u))))$
50	49	pm2.43d	$⊢ (u \in ω \land x \subseteq ⋃ x) \to (v \in x \to (F (suc u) = x \to v \in F (u)))$
51		id	$⊢ (F (suc u) = x \to v \in F (u)) \to (F (suc u) = x \to v \in F (u))$
52	51	necon3bd	$⊢ (F (suc u) = x \to v \in F (u)) \to (\neg v \in F (u) \to F (suc u) \neq x)$
53	50 52	syl6	$⊢ (u \in ω \land x \subseteq ⋃ x) \to (v \in x \to (\neg v \in F (u) \to F (suc u) \neq x))$
54	53	impd	$⊢ (u \in ω \land x \subseteq ⋃ x) \to ((v \in x \land \neg v \in F (u)) \to F (suc u) \neq x)$
55	54	exlimdv	$⊢ (u \in ω \land x \subseteq ⋃ x) \to (\exists v (v \in x \land \neg v \in F (u)) \to F (suc u) \neq x)$
56	27 55	syl5	$⊢ (u \in ω \land x \subseteq ⋃ x) \to ((F (u) \subseteq x \land F (u) \neq x) \to F (suc u) \neq x)$
57	24 56	sylani	$⊢ (u \in ω \land x \subseteq ⋃ x) \to ((u \in ω \land F (u) \neq x) \to F (suc u) \neq x)$
58	57	exp4b	$⊢ u \in ω \to (x \subseteq ⋃ x \to (u \in ω \to (F (u) \neq x \to F (suc u) \neq x)))$
59	58	pm2.43a	$⊢ u \in ω \to (x \subseteq ⋃ x \to (F (u) \neq x \to F (suc u) \neq x))$
60	59	adantld	$⊢ u \in ω \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to (F (u) \neq x \to F (suc u) \neq x))$
61	60	a2d	$⊢ u \in ω \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (u) \neq x) \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (suc u) \neq x))$
62	7 10 13 16 22 61	finds	$⊢ A \in ω \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (A) \neq x)$
63	62	com12	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to (A \in ω \to F (A) \neq x)$

Metamath Proof Explorer

Theorem inf3lem2

Proof