# Metamath Proof Explorer

## Theorem dnwech

Description: Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f ${⊢}{F}=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)$
dnnumch.a ${⊢}{\phi }\to {A}\in {V}$
dnnumch.g ${⊢}{\phi }\to \forall {y}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({y}\ne \varnothing \to {G}\left({y}\right)\in {y}\right)$
dnwech.h ${⊢}{H}=\left\{⟨{v},{w}⟩|\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right\}$
Assertion dnwech ${⊢}{\phi }\to {H}\mathrm{We}{A}$

### Proof

Step Hyp Ref Expression
1 dnnumch.f ${⊢}{F}=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)$
2 dnnumch.a ${⊢}{\phi }\to {A}\in {V}$
3 dnnumch.g ${⊢}{\phi }\to \forall {y}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({y}\ne \varnothing \to {G}\left({y}\right)\in {y}\right)$
4 dnwech.h ${⊢}{H}=\left\{⟨{v},{w}⟩|\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right\}$
5 1 2 3 dnnumch3 ${⊢}{\phi }\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1}{⟶}\mathrm{On}$
6 f1f1orn ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1}{⟶}\mathrm{On}\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)$
7 5 6 syl ${⊢}{\phi }\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)$
8 f1f ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1}{⟶}\mathrm{On}\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}⟶\mathrm{On}$
9 frn ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}⟶\mathrm{On}\to \mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\subseteq \mathrm{On}$
10 5 8 9 3syl ${⊢}{\phi }\to \mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\subseteq \mathrm{On}$
11 epweon ${⊢}\mathrm{E}\mathrm{We}\mathrm{On}$
12 wess ${⊢}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\subseteq \mathrm{On}\to \left(\mathrm{E}\mathrm{We}\mathrm{On}\to \mathrm{E}\mathrm{We}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\right)$
13 10 11 12 mpisyl ${⊢}{\phi }\to \mathrm{E}\mathrm{We}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)$
14 eqid ${⊢}\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}=\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}$
15 14 f1owe ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1 onto}{⟶}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\to \left(\mathrm{E}\mathrm{We}\mathrm{ran}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\to \left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\mathrm{We}{A}\right)$
16 7 13 15 sylc ${⊢}{\phi }\to \left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\mathrm{We}{A}$
17 fvex ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\in \mathrm{V}$
18 17 epeli ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)↔\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\in \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)$
19 1 2 3 dnnumch3lem ${⊢}\left({\phi }\wedge {v}\in {A}\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]$
20 19 adantrr ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]$
21 1 2 3 dnnumch3lem ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]$
22 21 adantrl ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]$
23 20 22 eleq12d ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left(\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\in \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)↔\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)$
24 18 23 syl5rbb ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]↔\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right)$
25 24 pm5.32da ${⊢}{\phi }\to \left(\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)↔\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right)\right)$
26 25 opabbidv ${⊢}{\phi }\to \left\{⟨{v},{w}⟩|\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\right\}=\left\{⟨{v},{w}⟩|\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right)\right\}$
27 incom ${⊢}{H}\cap \left({A}×{A}\right)=\left({A}×{A}\right)\cap {H}$
28 df-xp ${⊢}{A}×{A}=\left\{⟨{v},{w}⟩|\left({v}\in {A}\wedge {w}\in {A}\right)\right\}$
29 28 4 ineq12i ${⊢}\left({A}×{A}\right)\cap {H}=\left\{⟨{v},{w}⟩|\left({v}\in {A}\wedge {w}\in {A}\right)\right\}\cap \left\{⟨{v},{w}⟩|\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right\}$
30 inopab ${⊢}\left\{⟨{v},{w}⟩|\left({v}\in {A}\wedge {w}\in {A}\right)\right\}\cap \left\{⟨{v},{w}⟩|\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right\}=\left\{⟨{v},{w}⟩|\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\right\}$
31 27 29 30 3eqtri ${⊢}{H}\cap \left({A}×{A}\right)=\left\{⟨{v},{w}⟩|\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\right\}$
32 incom ${⊢}\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)=\left({A}×{A}\right)\cap \left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}$
33 28 ineq1i ${⊢}\left({A}×{A}\right)\cap \left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}=\left\{⟨{v},{w}⟩|\left({v}\in {A}\wedge {w}\in {A}\right)\right\}\cap \left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}$
34 inopab ${⊢}\left\{⟨{v},{w}⟩|\left({v}\in {A}\wedge {w}\in {A}\right)\right\}\cap \left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}=\left\{⟨{v},{w}⟩|\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right)\right\}$
35 32 33 34 3eqtri ${⊢}\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)=\left\{⟨{v},{w}⟩|\left(\left({v}\in {A}\wedge {w}\in {A}\right)\wedge \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right)\right\}$
36 26 31 35 3eqtr4g ${⊢}{\phi }\to {H}\cap \left({A}×{A}\right)=\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)$
37 weeq1 ${⊢}{H}\cap \left({A}×{A}\right)=\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)\to \left(\left({H}\cap \left({A}×{A}\right)\right)\mathrm{We}{A}↔\left(\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)\right)\mathrm{We}{A}\right)$
38 36 37 syl ${⊢}{\phi }\to \left(\left({H}\cap \left({A}×{A}\right)\right)\mathrm{We}{A}↔\left(\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)\right)\mathrm{We}{A}\right)$
39 weinxp ${⊢}{H}\mathrm{We}{A}↔\left({H}\cap \left({A}×{A}\right)\right)\mathrm{We}{A}$
40 weinxp ${⊢}\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\mathrm{We}{A}↔\left(\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\cap \left({A}×{A}\right)\right)\mathrm{We}{A}$
41 38 39 40 3bitr4g ${⊢}{\phi }\to \left({H}\mathrm{We}{A}↔\left\{⟨{v},{w}⟩|\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)\mathrm{E}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\right\}\mathrm{We}{A}\right)$
42 16 41 mpbird ${⊢}{\phi }\to {H}\mathrm{We}{A}$