inf3lem5

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	inf3lem5	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ((A \in ω \land B \in A) \to F (B) \subset F (A))$

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		elnn	$⊢ (B \in A \land A \in ω) \to B \in ω$
6	5	ancoms	$⊢ (A \in ω \land B \in A) \to B \in ω$
7		nnord	$⊢ A \in ω \to Ord A$
8		ordsucss	$⊢ Ord A \to (B \in A \to suc B \subseteq A)$
9	7 8	syl	$⊢ A \in ω \to (B \in A \to suc B \subseteq A)$
10	9	adantr	$⊢ (A \in ω \land B \in ω) \to (B \in A \to suc B \subseteq A)$
11		peano2b	$⊢ B \in ω \leftrightarrow suc B \in ω$
12		fveq2	$⊢ v = suc B \to F (v) = F (suc B)$
13	12	psseq2d	$⊢ v = suc B \to (F (B) \subset F (v) \leftrightarrow F (B) \subset F (suc B))$
14	13	imbi2d	$⊢ v = suc B \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (v)) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (suc B)))$
15		fveq2	$⊢ v = u \to F (v) = F (u)$
16	15	psseq2d	$⊢ v = u \to (F (B) \subset F (v) \leftrightarrow F (B) \subset F (u))$
17	16	imbi2d	$⊢ v = u \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (v)) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (u)))$
18		fveq2	$⊢ v = suc u \to F (v) = F (suc u)$
19	18	psseq2d	$⊢ v = suc u \to (F (B) \subset F (v) \leftrightarrow F (B) \subset F (suc u))$
20	19	imbi2d	$⊢ v = suc u \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (v)) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (suc u)))$
21		fveq2	$⊢ v = A \to F (v) = F (A)$
22	21	psseq2d	$⊢ v = A \to (F (B) \subset F (v) \leftrightarrow F (B) \subset F (A))$
23	22	imbi2d	$⊢ v = A \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (v)) \leftrightarrow ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A)))$
24	1 2 4 4	inf3lem4	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to (B \in ω \to F (B) \subset F (suc B))$
25	24	com12	$⊢ B \in ω \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (suc B))$
26	11 25	sylbir	$⊢ suc B \in ω \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (suc B))$
27		vex	$⊢ u \in V$
28	1 2 27 4	inf3lem4	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to (u \in ω \to F (u) \subset F (suc u))$
29		psstr	$⊢ (F (B) \subset F (u) \land F (u) \subset F (suc u)) \to F (B) \subset F (suc u)$
30	29	expcom	$⊢ F (u) \subset F (suc u) \to (F (B) \subset F (u) \to F (B) \subset F (suc u))$
31	28 30	syl6com	$⊢ u \in ω \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to (F (B) \subset F (u) \to F (B) \subset F (suc u)))$
32	31	a2d	$⊢ u \in ω \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (u)) \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (suc u)))$
33	32	ad2antrr	$⊢ ((u \in ω \land suc B \in ω) \land suc B \subseteq u) \to (((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (u)) \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (suc u)))$
34	14 17 20 23 26 33	findsg	$⊢ ((A \in ω \land suc B \in ω) \land suc B \subseteq A) \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A))$
35	34	ex	$⊢ (A \in ω \land suc B \in ω) \to (suc B \subseteq A \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A)))$
36	11 35	sylan2b	$⊢ (A \in ω \land B \in ω) \to (suc B \subseteq A \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A)))$
37	10 36	syld	$⊢ (A \in ω \land B \in ω) \to (B \in A \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A)))$
38	37	impancom	$⊢ (A \in ω \land B \in A) \to (B \in ω \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A)))$
39	6 38	mpd	$⊢ (A \in ω \land B \in A) \to ((x \neq \emptyset \land x \subseteq ⋃ x) \to F (B) \subset F (A))$
40	39	com12	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ((A \in ω \land B \in A) \to F (B) \subset F (A))$

Metamath Proof Explorer

Theorem inf3lem5

Proof