inf3lema

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	inf3lema	$⊢ A \in G (B) \leftrightarrow (A \in x \land A \cap x \subseteq B)$

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		ineq1	$⊢ f = A \to f \cap x = A \cap x$
6	5	sseq1d	$⊢ f = A \to (f \cap x \subseteq B \leftrightarrow A \cap x \subseteq B)$
7		sseq2	$⊢ v = B \to (f \cap x \subseteq v \leftrightarrow f \cap x \subseteq B)$
8	7	rabbidv	$⊢ v = B \to \{f \in x \| f \cap x \subseteq v\} = \{f \in x \| f \cap x \subseteq B\}$
9		sseq2	$⊢ y = v \to (w \cap x \subseteq y \leftrightarrow w \cap x \subseteq v)$
10	9	rabbidv	$⊢ y = v \to \{w \in x \| w \cap x \subseteq y\} = \{w \in x \| w \cap x \subseteq v\}$
11		ineq1	$⊢ w = f \to w \cap x = f \cap x$
12	11	sseq1d	$⊢ w = f \to (w \cap x \subseteq v \leftrightarrow f \cap x \subseteq v)$
13	12	cbvrabv	$⊢ \{w \in x \| w \cap x \subseteq v\} = \{f \in x \| f \cap x \subseteq v\}$
14	10 13	eqtrdi	$⊢ y = v \to \{w \in x \| w \cap x \subseteq y\} = \{f \in x \| f \cap x \subseteq v\}$
15	14	cbvmptv	$⊢ (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\}) = (v \in V ⟼ \{f \in x \| f \cap x \subseteq v\})$
16	1 15	eqtri	$⊢ G = (v \in V ⟼ \{f \in x \| f \cap x \subseteq v\})$
17		vex	$⊢ x \in V$
18	17	rabex	$⊢ \{f \in x \| f \cap x \subseteq B\} \in V$
19	8 16 18	fvmpt	$⊢ B \in V \to G (B) = \{f \in x \| f \cap x \subseteq B\}$
20	4 19	ax-mp	$⊢ G (B) = \{f \in x \| f \cap x \subseteq B\}$
21	6 20	elrab2	$⊢ A \in G (B) \leftrightarrow (A \in x \land A \cap x \subseteq B)$

Metamath Proof Explorer