Theorem 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\left(x\right)\to S=U$$
	fnwe2.t	$$⊢T=\left\{⟨x,y⟩|\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\right\}$$
	fnwe2.s	$$⊢\left(\phi \wedge x\in A\right)\to U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
	fnwe2.f	$$⊢\phi \to \left({F\upharpoonright }_A\right):A⟶B$$
	fnwe2.r	$$⊢\phi \to R\mathrm{We}B$$
Assertion	fnwe2	$$⊢\phi \to T\mathrm{We}A$$

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	$$⊢z=F\left(x\right)\to S=U$$
2		fnwe2.t	$$⊢T=\left\{⟨x,y⟩|\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\right\}$$
3		fnwe2.s	$$⊢\left(\phi \wedge x\in A\right)\to U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
4		fnwe2.f	$$⊢\phi \to \left({F\upharpoonright }_A\right):A⟶B$$
5		fnwe2.r	$$⊢\phi \to R\mathrm{We}B$$
6	3	adantlr	$$⊢\left(\left(\phi \wedge \left(a\subseteq A\wedge a\ne \varnothing \right)\right)\wedge x\in A\right)\to U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
7	4	adantr	$$⊢\left(\phi \wedge \left(a\subseteq A\wedge a\ne \varnothing \right)\right)\to \left({F\upharpoonright }_A\right):A⟶B$$
8	5	adantr	$$⊢\left(\phi \wedge \left(a\subseteq A\wedge a\ne \varnothing \right)\right)\to R\mathrm{We}B$$
9		simprl	$$⊢\left(\phi \wedge \left(a\subseteq A\wedge a\ne \varnothing \right)\right)\to a\subseteq A$$
10		simprr	$$⊢\left(\phi \wedge \left(a\subseteq A\wedge a\ne \varnothing \right)\right)\to a\ne \varnothing$$
11	1 2 6 7 8 9 10	fnwe2lem2	$$⊢\left(\phi \wedge \left(a\subseteq A\wedge a\ne \varnothing \right)\right)\to \exists c\in a\forall d\in a\neg dTc$$
12	11	ex	$$⊢\phi \to \left(\left(a\subseteq A\wedge a\ne \varnothing \right)\to \exists c\in a\forall d\in a\neg dTc\right)$$
13	12	alrimiv	$$⊢\phi \to \forall a\left(\left(a\subseteq A\wedge a\ne \varnothing \right)\to \exists c\in a\forall d\in a\neg dTc\right)$$
14		df-fr	$$⊢T\mathrm{Fr}A\leftrightarrow \forall a\left(\left(a\subseteq A\wedge a\ne \varnothing \right)\to \exists c\in a\forall d\in a\neg dTc\right)$$
15	13 14	sylibr	$$⊢\phi \to T\mathrm{Fr}A$$
16	3	adantlr	$$⊢\left(\left(\phi \wedge \left(a\in A\wedge b\in A\right)\right)\wedge x\in A\right)\to U\mathrm{We}\left\{y\in A|F\left(y\right)=F\left(x\right)\right\}$$
17	4	adantr	$$⊢\left(\phi \wedge \left(a\in A\wedge b\in A\right)\right)\to \left({F\upharpoonright }_A\right):A⟶B$$
18	5	adantr	$$⊢\left(\phi \wedge \left(a\in A\wedge b\in A\right)\right)\to R\mathrm{We}B$$
19		simprl	$$⊢\left(\phi \wedge \left(a\in A\wedge b\in A\right)\right)\to a\in A$$
20		simprr	$$⊢\left(\phi \wedge \left(a\in A\wedge b\in A\right)\right)\to b\in A$$
21	1 2 16 17 18 19 20	fnwe2lem3	$$⊢\left(\phi \wedge \left(a\in A\wedge b\in A\right)\right)\to \left(aTb\vee a=b\vee bTa\right)$$
22	21	ralrimivva	$$⊢\phi \to \forall a\in A\forall b\in A\left(aTb\vee a=b\vee bTa\right)$$
23		dfwe2	$$⊢T\mathrm{We}A\leftrightarrow \left(T\mathrm{Fr}A\wedge \forall a\in A\forall b\in A\left(aTb\vee a=b\vee bTa\right)\right)$$
24	15 22 23	sylanbrc	$$⊢\phi \to T\mathrm{We}A$$