hartogslem2

	Ref	Expression
Hypotheses	hartogslem.2	$⊢ F = \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
	hartogslem.3	$⊢ R = \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = f (w) \land t = f (z)) \land w E z)\}$
Assertion	hartogslem2	$⊢ A \in V \to \{x \in On \| x ≼ A\} \in V$

Step	Hyp	Ref	Expression
1		hartogslem.2	$⊢ F = \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
2		hartogslem.3	$⊢ R = \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = f (w) \land t = f (z)) \land w E z)\}$
3	1 2	hartogslem1	$⊢ (dom F \subseteq 𝒫 (A \times A) \land Fun F \land (A \in V \to ran F = \{x \in On \| x ≼ A\}))$
4	3	simp3i	$⊢ A \in V \to ran F = \{x \in On \| x ≼ A\}$
5	3	simp2i	$⊢ Fun F$
6	3	simp1i	$⊢ dom F \subseteq 𝒫 (A \times A)$
7		sqxpexg	$⊢ A \in V \to A \times A \in V$
8	7	pwexd	$⊢ A \in V \to 𝒫 (A \times A) \in V$
9		ssexg	$⊢ (dom F \subseteq 𝒫 (A \times A) \land 𝒫 (A \times A) \in V) \to dom F \in V$
10	6 8 9	sylancr	$⊢ A \in V \to dom F \in V$
11		funex	$⊢ (Fun F \land dom F \in V) \to F \in V$
12	5 10 11	sylancr	$⊢ A \in V \to F \in V$
13		rnexg	$⊢ F \in V \to ran F \in V$
14	12 13	syl	$⊢ A \in V \to ran F \in V$
15	4 14	eqeltrrd	$⊢ A \in V \to \{x \in On \| x ≼ A\} \in V$

Metamath Proof Explorer