harwdom

Description: The value of the Hartogs function at a set X is weakly dominated by ~P ( X X. X ) . This follows from a more precise analysis of the bound used in hartogs to prove that ( harX ) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	harwdom	$⊢ X \in V \to har (X) ≼^{*} 𝒫 (X \times X)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} = \{⟨r, y⟩ \| (((dom r \subseteq X \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		eqid	$⊢ \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = f (w) \land t = f (z)) \land w E z)\} = \{⟨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 \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \subseteq 𝒫 (X \times X) \land Fun \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \land (X \in V \to ran \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} = \{x \in On \| x ≼ X\}))$
4	3	simp2i	$⊢ Fun \{⟨r, y⟩ \| (((dom r \subseteq X \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))\}$
5	3	simp1i	$⊢ dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \subseteq 𝒫 (X \times X)$
6		sqxpexg	$⊢ X \in V \to X \times X \in V$
7	6	pwexd	$⊢ X \in V \to 𝒫 (X \times X) \in V$
8		ssexg	$⊢ (dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \subseteq 𝒫 (X \times X) \land 𝒫 (X \times X) \in V) \to dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \in V$
9	5 7 8	sylancr	$⊢ X \in V \to dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \in V$
10		funex	$⊢ (Fun \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \land dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \in V) \to \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \in V$
11	4 9 10	sylancr	$⊢ X \in V \to \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \in V$
12		funfn	$⊢ Fun \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \leftrightarrow \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} Fn dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\}$
13	4 12	mpbi	$⊢ \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} Fn dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\}$
14	13	a1i	$⊢ X \in V \to \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} Fn dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\}$
15	3	simp3i	$⊢ X \in V \to ran \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} = \{x \in On \| x ≼ X\}$
16		harval	$⊢ X \in V \to har (X) = \{x \in On \| x ≼ X\}$
17	15 16	eqtr4d	$⊢ X \in V \to ran \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} = har (X)$
18		df-fo	$⊢ \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} : dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \underset{onto}{⟶} har (X) \leftrightarrow (\{⟨r, y⟩ \| (((dom r \subseteq X \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))\} Fn dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \land ran \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} = har (X))$
19	14 17 18	sylanbrc	$⊢ X \in V \to \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} : dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \underset{onto}{⟶} har (X)$
20		fowdom	$⊢ (\{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \in V \land \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} : dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \underset{onto}{⟶} har (X)) \to har (X) ≼^{*} dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\}$
21	11 19 20	syl2anc	$⊢ X \in V \to har (X) ≼^{*} dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\}$
22		ssdomg	$⊢ 𝒫 (X \times X) \in V \to (dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \subseteq 𝒫 (X \times X) \to dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} ≼ 𝒫 (X \times X))$
23	7 5 22	mpisyl	$⊢ X \in V \to dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} ≼ 𝒫 (X \times X)$
24		domwdom	$⊢ dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} ≼ 𝒫 (X \times X) \to dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} ≼^{*} 𝒫 (X \times X)$
25	23 24	syl	$⊢ X \in V \to dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} ≼^{*} 𝒫 (X \times X)$
26		wdomtr	$⊢ (har (X) ≼^{} dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} \land dom \{⟨r, y⟩ \| (((dom r \subseteq X \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))\} ≼^{} 𝒫 (X \times X)) \to har (X) ≼^{*} 𝒫 (X \times X)$
27	21 25 26	syl2anc	$⊢ X \in V \to har (X) ≼^{*} 𝒫 (X \times X)$

Metamath Proof Explorer

Theorem harwdom

Proof