fnwe2

Description: A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	fnwe2.su	$⊢ z = F (x) \to S = U$
	fnwe2.t	$⊢ T = \{⟨x, y⟩ \| (F (x) R F (y) \lor (F (x) = F (y) \land x U y))\}$
	fnwe2.s	$⊢ (φ \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
	fnwe2.f	$⊢ φ \to ({F ↾}_{A}) : A ⟶ B$
	fnwe2.r	$⊢ φ \to R We B$
Assertion	fnwe2	$⊢ φ \to T We A$

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	$⊢ z = F (x) \to S = U$
2		fnwe2.t	$⊢ T = \{⟨x, y⟩ \| (F (x) R F (y) \lor (F (x) = F (y) \land x U y))\}$
3		fnwe2.s	$⊢ (φ \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
4		fnwe2.f	$⊢ φ \to ({F ↾}_{A}) : A ⟶ B$
5		fnwe2.r	$⊢ φ \to R We B$
6	3	adantlr	$⊢ ((φ \land (a \subseteq A \land a \neq \emptyset)) \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
7	4	adantr	$⊢ (φ \land (a \subseteq A \land a \neq \emptyset)) \to ({F ↾}_{A}) : A ⟶ B$
8	5	adantr	$⊢ (φ \land (a \subseteq A \land a \neq \emptyset)) \to R We B$
9		simprl	$⊢ (φ \land (a \subseteq A \land a \neq \emptyset)) \to a \subseteq A$
10		simprr	$⊢ (φ \land (a \subseteq A \land a \neq \emptyset)) \to a \neq \emptyset$
11	1 2 6 7 8 9 10	fnwe2lem2	$⊢ (φ \land (a \subseteq A \land a \neq \emptyset)) \to \exists c \in a \forall d \in a \neg d T c$
12	11	ex	$⊢ φ \to ((a \subseteq A \land a \neq \emptyset) \to \exists c \in a \forall d \in a \neg d T c)$
13	12	alrimiv	$⊢ φ \to \forall a ((a \subseteq A \land a \neq \emptyset) \to \exists c \in a \forall d \in a \neg d T c)$
14		df-fr	$⊢ T Fr A \leftrightarrow \forall a ((a \subseteq A \land a \neq \emptyset) \to \exists c \in a \forall d \in a \neg d T c)$
15	13 14	sylibr	$⊢ φ \to T Fr A$
16	3	adantlr	$⊢ ((φ \land (a \in A \land b \in A)) \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
17	4	adantr	$⊢ (φ \land (a \in A \land b \in A)) \to ({F ↾}_{A}) : A ⟶ B$
18	5	adantr	$⊢ (φ \land (a \in A \land b \in A)) \to R We B$
19		simprl	$⊢ (φ \land (a \in A \land b \in A)) \to a \in A$
20		simprr	$⊢ (φ \land (a \in A \land b \in A)) \to b \in A$
21	1 2 16 17 18 19 20	fnwe2lem3	$⊢ (φ \land (a \in A \land b \in A)) \to (a T b \lor a = b \lor b T a)$
22	21	ralrimivva	$⊢ φ \to \forall a \in A \forall b \in A (a T b \lor a = b \lor b T a)$
23		dfwe2	$⊢ T We A \leftrightarrow (T Fr A \land \forall a \in A \forall b \in A (a T b \lor a = b \lor b T a))$
24	15 22 23	sylanbrc	$⊢ φ \to T We A$

Metamath Proof Explorer

Theorem fnwe2

Proof