rankprb

Description: The rank of an unordered pair. Part of Exercise 30 of Enderton p. 207. (Contributed by Mario Carneiro, 10-Jun-2013)

		Ref	Expression
	Assertion	rankprb	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to rank (\{A, B\}) = suc (rank (A) \cup rank (B))$

Step	Hyp	Ref	Expression
1		snwf	$⊢ A \in ⋃ R_{1} [On] \to \{A\} \in ⋃ R_{1} [On]$
2		snwf	$⊢ B \in ⋃ R_{1} [On] \to \{B\} \in ⋃ R_{1} [On]$
3		rankunb	$⊢ (\{A\} \in ⋃ R_{1} [On] \land \{B\} \in ⋃ R_{1} [On]) \to rank (\{A\} \cup \{B\}) = rank (\{A\}) \cup rank (\{B\})$
4	1 2 3	syl2an	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to rank (\{A\} \cup \{B\}) = rank (\{A\}) \cup rank (\{B\})$
5		ranksnb	$⊢ A \in ⋃ R_{1} [On] \to rank (\{A\}) = suc rank (A)$
6		ranksnb	$⊢ B \in ⋃ R_{1} [On] \to rank (\{B\}) = suc rank (B)$
7		uneq12	$⊢ (rank (\{A\}) = suc rank (A) \land rank (\{B\}) = suc rank (B)) \to rank (\{A\}) \cup rank (\{B\}) = suc rank (A) \cup suc rank (B)$
8	5 6 7	syl2an	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to rank (\{A\}) \cup rank (\{B\}) = suc rank (A) \cup suc rank (B)$
9	4 8	eqtrd	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to rank (\{A\} \cup \{B\}) = suc rank (A) \cup suc rank (B)$
10		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
11	10	fveq2i	$⊢ rank (\{A, B\}) = rank (\{A\} \cup \{B\})$
12		rankon	$⊢ rank (A) \in On$
13	12	onordi	$⊢ Ord rank (A)$
14		rankon	$⊢ rank (B) \in On$
15	14	onordi	$⊢ Ord rank (B)$
16		ordsucun	$⊢ (Ord rank (A) \land Ord rank (B)) \to suc (rank (A) \cup rank (B)) = suc rank (A) \cup suc rank (B)$
17	13 15 16	mp2an	$⊢ suc (rank (A) \cup rank (B)) = suc rank (A) \cup suc rank (B)$
18	9 11 17	3eqtr4g	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to rank (\{A, B\}) = suc (rank (A) \cup rank (B))$

Metamath Proof Explorer