Theorem cardpred

Description: The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024)

	Ref	Expression
Assertion	cardpred	⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card ) → Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝐵 ) ) = ( card “ Pred ( ≺ , 𝐴 , 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cardf2	⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On
2		ffun	⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card )
3	2	funfnd	⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → card Fn dom card )
4	1 3	mp1i	⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card ) → card Fn dom card )
5		fvex	⊢ ( card ‘ 𝑦 ) ∈ V
6	5	epeli	⊢ ( ( card ‘ 𝑥 ) E ( card ‘ 𝑦 ) ↔ ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) )
7		cardsdom2	⊢ ( ( 𝑥 ∈ dom card ∧ 𝑦 ∈ dom card ) → ( ( card ‘ 𝑥 ) ∈ ( card ‘ 𝑦 ) ↔ 𝑥 ≺ 𝑦 ) )
8	6 7	bitr2id	⊢ ( ( 𝑥 ∈ dom card ∧ 𝑦 ∈ dom card ) → ( 𝑥 ≺ 𝑦 ↔ ( card ‘ 𝑥 ) E ( card ‘ 𝑦 ) ) )
9	8	rgen2	⊢ ∀ 𝑥 ∈ dom card ∀ 𝑦 ∈ dom card ( 𝑥 ≺ 𝑦 ↔ ( card ‘ 𝑥 ) E ( card ‘ 𝑦 ) )
10	9	a1i	⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card ) → ∀ 𝑥 ∈ dom card ∀ 𝑦 ∈ dom card ( 𝑥 ≺ 𝑦 ↔ ( card ‘ 𝑥 ) E ( card ‘ 𝑦 ) ) )
11		simpl	⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card ) → 𝐴 ⊆ dom card )
12		simpr	⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card ) → 𝐵 ∈ dom card )
13	4 10 11 12	fnrelpredd	⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card ) → Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝐵 ) ) = ( card “ Pred ( ≺ , 𝐴 , 𝐵 ) ) )