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