harval3

Description: ( harA ) is the least cardinal that is greater than A . (Contributed by RP, 4-Nov-2023)

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

Proof

Step	Hyp	Ref	Expression
1		harval2	$⊢ A \in dom card \to har (A) = ⋂ \{y \in On \| A ≺ y\}$
2		vex	$⊢ x \in V$
3	2	a1i	$⊢ A \in dom card \to x \in V$
4		elrncard	$⊢ x \in ran card \leftrightarrow (x \in On \land \forall y \in x \neg y \approx x)$
5	4	simplbi	$⊢ x \in ran card \to x \in On$
6	5	anim1i	$⊢ (x \in ran card \land A ≺ x) \to (x \in On \land A ≺ x)$
7		eleq1	$⊢ y = x \to (y \in On \leftrightarrow x \in On)$
8		breq2	$⊢ y = x \to (A ≺ y \leftrightarrow A ≺ x)$
9	7 8	anbi12d	$⊢ y = x \to ((y \in On \land A ≺ y) \leftrightarrow (x \in On \land A ≺ x))$
10	6 9	imbitrrid	$⊢ y = x \to ((x \in ran card \land A ≺ x) \to (y \in On \land A ≺ y))$
11	10	adantl	$⊢ (A \in dom card \land y = x) \to ((x \in ran card \land A ≺ x) \to (y \in On \land A ≺ y))$
12		ssidd	$⊢ A \in dom card \to x \subseteq x$
13	3 11 12	intabssd	$⊢ A \in dom card \to ⋂ \{y \| (y \in On \land A ≺ y)\} \subseteq ⋂ \{x \| (x \in ran card \land A ≺ x)\}$
14		vex	$⊢ y \in V$
15	14	inex1	$⊢ y \cap card (y) \in V$
16	15	a1i	$⊢ A \in dom card \to y \cap card (y) \in V$
17		oncardid	$⊢ y \in On \to card (y) \approx y$
18	17	ensymd	$⊢ y \in On \to y \approx card (y)$
19		sdomentr	$⊢ (A ≺ y \land y \approx card (y)) \to A ≺ card (y)$
20	19	a1i	$⊢ y \in On \to ((A ≺ y \land y \approx card (y)) \to A ≺ card (y))$
21	18 20	mpan2d	$⊢ y \in On \to (A ≺ y \to A ≺ card (y))$
22		df-card	$⊢ card = (x \in V ⟼ ⋂ \{y \in On \| y \approx x\})$
23	22	funmpt2	$⊢ Fun card$
24		onenon	$⊢ y \in On \to y \in dom card$
25		fvelrn	$⊢ (Fun card \land y \in dom card) \to card (y) \in ran card$
26	23 24 25	sylancr	$⊢ y \in On \to card (y) \in ran card$
27	21 26	jctild	$⊢ y \in On \to (A ≺ y \to (card (y) \in ran card \land A ≺ card (y)))$
28	27	adantl	$⊢ (x = y \cap card (y) \land y \in On) \to (A ≺ y \to (card (y) \in ran card \land A ≺ card (y)))$
29		simpl	$⊢ (x = y \cap card (y) \land y \in On) \to x = y \cap card (y)$
30		cardonle	$⊢ y \in On \to card (y) \subseteq y$
31	30	adantl	$⊢ (x = y \cap card (y) \land y \in On) \to card (y) \subseteq y$
32		sseqin2	$⊢ card (y) \subseteq y \leftrightarrow y \cap card (y) = card (y)$
33	31 32	sylib	$⊢ (x = y \cap card (y) \land y \in On) \to y \cap card (y) = card (y)$
34	29 33	eqtrd	$⊢ (x = y \cap card (y) \land y \in On) \to x = card (y)$
35		eleq1	$⊢ x = card (y) \to (x \in ran card \leftrightarrow card (y) \in ran card)$
36		breq2	$⊢ x = card (y) \to (A ≺ x \leftrightarrow A ≺ card (y))$
37	35 36	anbi12d	$⊢ x = card (y) \to ((x \in ran card \land A ≺ x) \leftrightarrow (card (y) \in ran card \land A ≺ card (y)))$
38	34 37	syl	$⊢ (x = y \cap card (y) \land y \in On) \to ((x \in ran card \land A ≺ x) \leftrightarrow (card (y) \in ran card \land A ≺ card (y)))$
39	28 38	sylibrd	$⊢ (x = y \cap card (y) \land y \in On) \to (A ≺ y \to (x \in ran card \land A ≺ x))$
40	39	expimpd	$⊢ x = y \cap card (y) \to ((y \in On \land A ≺ y) \to (x \in ran card \land A ≺ x))$
41	40	adantl	$⊢ (A \in dom card \land x = y \cap card (y)) \to ((y \in On \land A ≺ y) \to (x \in ran card \land A ≺ x))$
42		inss1	$⊢ y \cap card (y) \subseteq y$
43	42	a1i	$⊢ A \in dom card \to y \cap card (y) \subseteq y$
44	16 41 43	intabssd	$⊢ A \in dom card \to ⋂ \{x \| (x \in ran card \land A ≺ x)\} \subseteq ⋂ \{y \| (y \in On \land A ≺ y)\}$
45	13 44	eqssd	$⊢ A \in dom card \to ⋂ \{y \| (y \in On \land A ≺ y)\} = ⋂ \{x \| (x \in ran card \land A ≺ x)\}$
46		df-rab	$⊢ \{y \in On \| A ≺ y\} = \{y \| (y \in On \land A ≺ y)\}$
47	46	inteqi	$⊢ ⋂ \{y \in On \| A ≺ y\} = ⋂ \{y \| (y \in On \land A ≺ y)\}$
48		df-rab	$⊢ \{x \in ran card \| A ≺ x\} = \{x \| (x \in ran card \land A ≺ x)\}$
49	48	inteqi	$⊢ ⋂ \{x \in ran card \| A ≺ x\} = ⋂ \{x \| (x \in ran card \land A ≺ x)\}$
50	45 47 49	3eqtr4g	$⊢ A \in dom card \to ⋂ \{y \in On \| A ≺ y\} = ⋂ \{x \in ran card \| A ≺ x\}$
51	1 50	eqtrd	$⊢ A \in dom card \to har (A) = ⋂ \{x \in ran card \| A ≺ x\}$

Metamath Proof Explorer

Theorem harval3

Proof