harval2

Description: An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	harval2	$⊢ A \in dom card \to har (A) = ⋂ \{x \in On \| A ≺ x\}$

Proof

Step	Hyp	Ref	Expression
1		harval	$⊢ A \in dom card \to har (A) = \{y \in On \| y ≼ A\}$
2	1	adantr	$⊢ (A \in dom card \land (x \in On \land A ≺ x)) \to har (A) = \{y \in On \| y ≼ A\}$
3		sdomel	$⊢ (y \in On \land x \in On) \to (y ≺ x \to y \in x)$
4		domsdomtr	$⊢ (y ≼ A \land A ≺ x) \to y ≺ x$
5	3 4	impel	$⊢ ((y \in On \land x \in On) \land (y ≼ A \land A ≺ x)) \to y \in x$
6	5	an4s	$⊢ ((y \in On \land y ≼ A) \land (x \in On \land A ≺ x)) \to y \in x$
7	6	ancoms	$⊢ ((x \in On \land A ≺ x) \land (y \in On \land y ≼ A)) \to y \in x$
8	7	3impb	$⊢ ((x \in On \land A ≺ x) \land y \in On \land y ≼ A) \to y \in x$
9	8	rabssdv	$⊢ (x \in On \land A ≺ x) \to \{y \in On \| y ≼ A\} \subseteq x$
10	9	adantl	$⊢ (A \in dom card \land (x \in On \land A ≺ x)) \to \{y \in On \| y ≼ A\} \subseteq x$
11	2 10	eqsstrd	$⊢ (A \in dom card \land (x \in On \land A ≺ x)) \to har (A) \subseteq x$
12	11	expr	$⊢ (A \in dom card \land x \in On) \to (A ≺ x \to har (A) \subseteq x)$
13	12	ralrimiva	$⊢ A \in dom card \to \forall x \in On (A ≺ x \to har (A) \subseteq x)$
14		ssintrab	$⊢ har (A) \subseteq ⋂ \{x \in On \| A ≺ x\} \leftrightarrow \forall x \in On (A ≺ x \to har (A) \subseteq x)$
15	13 14	sylibr	$⊢ A \in dom card \to har (A) \subseteq ⋂ \{x \in On \| A ≺ x\}$
16		breq2	$⊢ x = har (A) \to (A ≺ x \leftrightarrow A ≺ har (A))$
17		harcl	$⊢ har (A) \in On$
18	17	a1i	$⊢ A \in dom card \to har (A) \in On$
19		harsdom	$⊢ A \in dom card \to A ≺ har (A)$
20	16 18 19	elrabd	$⊢ A \in dom card \to har (A) \in \{x \in On \| A ≺ x\}$
21		intss1	$⊢ har (A) \in \{x \in On \| A ≺ x\} \to ⋂ \{x \in On \| A ≺ x\} \subseteq har (A)$
22	20 21	syl	$⊢ A \in dom card \to ⋂ \{x \in On \| A ≺ x\} \subseteq har (A)$
23	15 22	eqssd	$⊢ A \in dom card \to har (A) = ⋂ \{x \in On \| A ≺ x\}$

Metamath Proof Explorer

Theorem harval2

Proof