unwf

Description: A binary union is well-founded iff its elements are. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	unwf	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \leftrightarrow A \cup B \in ⋃ R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		r1rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq R_{1} (rank (A))$
2	1	adantr	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \subseteq R_{1} (rank (A))$
3		ssun1	$⊢ rank (A) \subseteq rank (A) \cup rank (B)$
4		rankdmr1	$⊢ rank (A) \in dom R_{1}$
5		r1dmlim	$⊢ Lim dom R_{1}$
6		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
7	5 6	ax-mp	$⊢ Ord dom R_{1}$
8		rankdmr1	$⊢ rank (B) \in dom R_{1}$
9		ordunel	$⊢ (Ord dom R_{1} \land rank (A) \in dom R_{1} \land rank (B) \in dom R_{1}) \to rank (A) \cup rank (B) \in dom R_{1}$
10	7 4 8 9	mp3an	$⊢ rank (A) \cup rank (B) \in dom R_{1}$
11		r1ord3g	$⊢ (rank (A) \in dom R_{1} \land rank (A) \cup rank (B) \in dom R_{1}) \to (rank (A) \subseteq rank (A) \cup rank (B) \to R_{1} (rank (A)) \subseteq R_{1} (rank (A) \cup rank (B)))$
12	4 10 11	mp2an	$⊢ rank (A) \subseteq rank (A) \cup rank (B) \to R_{1} (rank (A)) \subseteq R_{1} (rank (A) \cup rank (B))$
13	3 12	ax-mp	$⊢ R_{1} (rank (A)) \subseteq R_{1} (rank (A) \cup rank (B))$
14	2 13	sstrdi	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \subseteq R_{1} (rank (A) \cup rank (B))$
15		r1rankidb	$⊢ B \in ⋃ R_{1} [On] \to B \subseteq R_{1} (rank (B))$
16	15	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to B \subseteq R_{1} (rank (B))$
17		ssun2	$⊢ rank (B) \subseteq rank (A) \cup rank (B)$
18		r1ord3g	$⊢ (rank (B) \in dom R_{1} \land rank (A) \cup rank (B) \in dom R_{1}) \to (rank (B) \subseteq rank (A) \cup rank (B) \to R_{1} (rank (B)) \subseteq R_{1} (rank (A) \cup rank (B)))$
19	8 10 18	mp2an	$⊢ rank (B) \subseteq rank (A) \cup rank (B) \to R_{1} (rank (B)) \subseteq R_{1} (rank (A) \cup rank (B))$
20	17 19	ax-mp	$⊢ R_{1} (rank (B)) \subseteq R_{1} (rank (A) \cup rank (B))$
21	16 20	sstrdi	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to B \subseteq R_{1} (rank (A) \cup rank (B))$
22	14 21	unssd	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \cup B \subseteq R_{1} (rank (A) \cup rank (B))$
23		fvex	$⊢ R_{1} (rank (A) \cup rank (B)) \in V$
24	23	elpw2	$⊢ A \cup B \in 𝒫 R_{1} (rank (A) \cup rank (B)) \leftrightarrow A \cup B \subseteq R_{1} (rank (A) \cup rank (B))$
25	22 24	sylibr	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \cup B \in 𝒫 R_{1} (rank (A) \cup rank (B))$
26		r1sucg	$⊢ rank (A) \cup rank (B) \in dom R_{1} \to R_{1} (suc (rank (A) \cup rank (B))) = 𝒫 R_{1} (rank (A) \cup rank (B))$
27	10 26	ax-mp	$⊢ R_{1} (suc (rank (A) \cup rank (B))) = 𝒫 R_{1} (rank (A) \cup rank (B))$
28	25 27	eleqtrrdi	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \cup B \in R_{1} (suc (rank (A) \cup rank (B)))$
29		r1elwf	$⊢ A \cup B \in R_{1} (suc (rank (A) \cup rank (B))) \to A \cup B \in ⋃ R_{1} [On]$
30	28 29	syl	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \cup B \in ⋃ R_{1} [On]$
31		ssun1	$⊢ A \subseteq A \cup B$
32		sswf	$⊢ (A \cup B \in ⋃ R_{1} [On] \land A \subseteq A \cup B) \to A \in ⋃ R_{1} [On]$
33	31 32	mpan2	$⊢ A \cup B \in ⋃ R_{1} [On] \to A \in ⋃ R_{1} [On]$
34		ssun2	$⊢ B \subseteq A \cup B$
35		sswf	$⊢ (A \cup B \in ⋃ R_{1} [On] \land B \subseteq A \cup B) \to B \in ⋃ R_{1} [On]$
36	34 35	mpan2	$⊢ A \cup B \in ⋃ R_{1} [On] \to B \in ⋃ R_{1} [On]$
37	33 36	jca	$⊢ A \cup B \in ⋃ R_{1} [On] \to (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On])$
38	30 37	impbii	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \leftrightarrow A \cup B \in ⋃ R_{1} [On]$

Metamath Proof Explorer

Theorem unwf

Proof