# Metamath Proof Explorer

## Theorem unxpwdom2

Description: Lemma for unxpwdom . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion unxpwdom2 ${⊢}\left({A}×{A}\right)\approx \left({B}\cup {C}\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$

### Proof

Step Hyp Ref Expression
1 ensym ${⊢}\left({A}×{A}\right)\approx \left({B}\cup {C}\right)\to \left({B}\cup {C}\right)\approx \left({A}×{A}\right)$
2 bren ${⊢}\left({B}\cup {C}\right)\approx \left({A}×{A}\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}$
3 ssdif0 ${⊢}{A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]↔{A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]=\varnothing$
4 dmxpid ${⊢}\mathrm{dom}\left({A}×{A}\right)={A}$
5 f1ofo ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {f}:{B}\cup {C}\underset{onto}{⟶}{A}×{A}$
6 forn ${⊢}{f}:{B}\cup {C}\underset{onto}{⟶}{A}×{A}\to \mathrm{ran}{f}={A}×{A}$
7 5 6 syl ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \mathrm{ran}{f}={A}×{A}$
8 vex ${⊢}{f}\in \mathrm{V}$
9 8 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
10 7 9 eqeltrrdi ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {A}×{A}\in \mathrm{V}$
11 10 dmexd ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \mathrm{dom}\left({A}×{A}\right)\in \mathrm{V}$
12 4 11 eqeltrrid ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {A}\in \mathrm{V}$
13 imassrn ${⊢}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\subseteq \mathrm{ran}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)$
14 f1stres ${⊢}\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right):{A}×{A}⟶{A}$
15 f1of ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {f}:{B}\cup {C}⟶{A}×{A}$
16 fco ${⊢}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right):{A}×{A}⟶{A}\wedge {f}:{B}\cup {C}⟶{A}×{A}\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right):{B}\cup {C}⟶{A}$
17 14 15 16 sylancr ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right):{B}\cup {C}⟶{A}$
18 17 frnd ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \mathrm{ran}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\subseteq {A}$
19 13 18 sstrid ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\subseteq {A}$
20 12 19 ssexd ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\in \mathrm{V}$
21 20 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\in \mathrm{V}$
22 simpr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
23 ssdomg ${⊢}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\in \mathrm{V}\to \left({A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\to {A}\preccurlyeq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)$
24 21 22 23 sylc ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to {A}\preccurlyeq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
25 domwdom ${⊢}{A}\preccurlyeq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\to {A}{\preccurlyeq }^{*}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
26 24 25 syl ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to {A}{\preccurlyeq }^{*}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
27 17 ffund ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \mathrm{Fun}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)$
28 ssun1 ${⊢}{B}\subseteq {B}\cup {C}$
29 f1odm ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \mathrm{dom}{f}={B}\cup {C}$
30 8 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
31 29 30 eqeltrrdi ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {B}\cup {C}\in \mathrm{V}$
32 ssexg ${⊢}\left({B}\subseteq {B}\cup {C}\wedge {B}\cup {C}\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
33 28 31 32 sylancr ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {B}\in \mathrm{V}$
34 wdomima2g ${⊢}\left(\mathrm{Fun}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\wedge {B}\in \mathrm{V}\wedge \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\in \mathrm{V}\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]{\preccurlyeq }^{*}{B}$
35 27 33 20 34 syl3anc ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]{\preccurlyeq }^{*}{B}$
36 35 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]{\preccurlyeq }^{*}{B}$
37 wdomtr ${⊢}\left({A}{\preccurlyeq }^{*}\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\wedge \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]{\preccurlyeq }^{*}{B}\right)\to {A}{\preccurlyeq }^{*}{B}$
38 26 36 37 syl2anc ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to {A}{\preccurlyeq }^{*}{B}$
39 38 orcd ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$
40 39 ex ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({A}\subseteq \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)\right)$
41 3 40 syl5bir ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]=\varnothing \to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)\right)$
42 n0 ${⊢}{A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)$
43 ssun2 ${⊢}{C}\subseteq {B}\cup {C}$
44 ssexg ${⊢}\left({C}\subseteq {B}\cup {C}\wedge {B}\cup {C}\in \mathrm{V}\right)\to {C}\in \mathrm{V}$
45 43 31 44 sylancr ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {C}\in \mathrm{V}$
46 45 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {C}\in \mathrm{V}$
47 f1ofn ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {f}Fn\left({B}\cup {C}\right)$
48 elpreima ${⊢}{f}Fn\left({B}\cup {C}\right)\to \left({y}\in {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]↔\left({y}\in \left({B}\cup {C}\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\right)$
49 47 48 syl ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({y}\in {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]↔\left({y}\in \left({B}\cup {C}\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\right)$
50 49 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left({y}\in {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]↔\left({y}\in \left({B}\cup {C}\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\right)$
51 elun ${⊢}{y}\in \left({B}\cup {C}\right)↔\left({y}\in {B}\vee {y}\in {C}\right)$
52 df-or ${⊢}\left({y}\in {B}\vee {y}\in {C}\right)↔\left(¬{y}\in {B}\to {y}\in {C}\right)$
53 51 52 bitri ${⊢}{y}\in \left({B}\cup {C}\right)↔\left(¬{y}\in {B}\to {y}\in {C}\right)$
54 eldifn ${⊢}{x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to ¬{x}\in \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
55 54 ad2antlr ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\to ¬{x}\in \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
56 15 ad2antrr ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {f}:{B}\cup {C}⟶{A}×{A}$
57 simprr ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {y}\in {B}$
58 28 57 sseldi ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {y}\in \left({B}\cup {C}\right)$
59 fvco3 ${⊢}\left({f}:{B}\cup {C}⟶{A}×{A}\wedge {y}\in \left({B}\cup {C}\right)\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left({y}\right)=\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)$
60 56 58 59 syl2anc ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left({y}\right)=\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)$
61 eldifi ${⊢}{x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to {x}\in {A}$
62 61 adantl ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {x}\in {A}$
63 62 snssd ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left\{{x}\right\}\subseteq {A}$
64 xpss1 ${⊢}\left\{{x}\right\}\subseteq {A}\to \left\{{x}\right\}×{A}\subseteq {A}×{A}$
65 63 64 syl ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left\{{x}\right\}×{A}\subseteq {A}×{A}$
66 65 adantr ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left\{{x}\right\}×{A}\subseteq {A}×{A}$
67 simprl ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)$
68 66 67 sseldd ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {f}\left({y}\right)\in \left({A}×{A}\right)$
69 68 fvresd ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)={1}^{st}\left({f}\left({y}\right)\right)$
70 xp1st ${⊢}{f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\to {1}^{st}\left({f}\left({y}\right)\right)\in \left\{{x}\right\}$
71 67 70 syl ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {1}^{st}\left({f}\left({y}\right)\right)\in \left\{{x}\right\}$
72 69 71 eqeltrd ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)\in \left\{{x}\right\}$
73 elsni ${⊢}\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)\in \left\{{x}\right\}\to \left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)={x}$
74 72 73 syl ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\left({f}\left({y}\right)\right)={x}$
75 60 74 eqtrd ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left({y}\right)={x}$
76 17 ffnd ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)Fn\left({B}\cup {C}\right)$
77 76 ad2antrr ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)Fn\left({B}\cup {C}\right)$
78 28 a1i ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {B}\subseteq {B}\cup {C}$
79 fnfvima ${⊢}\left(\left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)Fn\left({B}\cup {C}\right)\wedge {B}\subseteq {B}\cup {C}\wedge {y}\in {B}\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left({y}\right)\in \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
80 77 78 57 79 syl3anc ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left({y}\right)\in \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
81 75 80 eqeltrrd ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\wedge {y}\in {B}\right)\right)\to {x}\in \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]$
82 81 expr ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\to \left({y}\in {B}\to {x}\in \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)$
83 55 82 mtod ${⊢}\left(\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\to ¬{y}\in {B}$
84 83 ex ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\to ¬{y}\in {B}\right)$
85 84 imim1d ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left(\left(¬{y}\in {B}\to {y}\in {C}\right)\to \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\to {y}\in {C}\right)\right)$
86 53 85 syl5bi ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left({y}\in \left({B}\cup {C}\right)\to \left({f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\to {y}\in {C}\right)\right)$
87 86 impd ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left(\left({y}\in \left({B}\cup {C}\right)\wedge {f}\left({y}\right)\in \left(\left\{{x}\right\}×{A}\right)\right)\to {y}\in {C}\right)$
88 50 87 sylbid ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left({y}\in {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\to {y}\in {C}\right)$
89 88 ssrdv ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\subseteq {C}$
90 ssdomg ${⊢}{C}\in \mathrm{V}\to \left({{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\subseteq {C}\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\preccurlyeq {C}\right)$
91 46 89 90 sylc ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\preccurlyeq {C}$
92 f1ocnv ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {{f}}^{-1}:{A}×{A}\underset{1-1 onto}{⟶}{B}\cup {C}$
93 f1of1 ${⊢}{{f}}^{-1}:{A}×{A}\underset{1-1 onto}{⟶}{B}\cup {C}\to {{f}}^{-1}:{A}×{A}\underset{1-1}{⟶}{B}\cup {C}$
94 92 93 syl ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to {{f}}^{-1}:{A}×{A}\underset{1-1}{⟶}{B}\cup {C}$
95 94 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {{f}}^{-1}:{A}×{A}\underset{1-1}{⟶}{B}\cup {C}$
96 31 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {B}\cup {C}\in \mathrm{V}$
97 snex ${⊢}\left\{{x}\right\}\in \mathrm{V}$
98 12 adantr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {A}\in \mathrm{V}$
99 xpexg ${⊢}\left(\left\{{x}\right\}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left\{{x}\right\}×{A}\in \mathrm{V}$
100 97 98 99 sylancr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left\{{x}\right\}×{A}\in \mathrm{V}$
101 f1imaen2g ${⊢}\left(\left({{f}}^{-1}:{A}×{A}\underset{1-1}{⟶}{B}\cup {C}\wedge {B}\cup {C}\in \mathrm{V}\right)\wedge \left(\left\{{x}\right\}×{A}\subseteq {A}×{A}\wedge \left\{{x}\right\}×{A}\in \mathrm{V}\right)\right)\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\approx \left(\left\{{x}\right\}×{A}\right)$
102 95 96 65 100 101 syl22anc ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\approx \left(\left\{{x}\right\}×{A}\right)$
103 vex ${⊢}{x}\in \mathrm{V}$
104 xpsnen2g ${⊢}\left({x}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left(\left\{{x}\right\}×{A}\right)\approx {A}$
105 103 98 104 sylancr ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left(\left\{{x}\right\}×{A}\right)\approx {A}$
106 entr ${⊢}\left({{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\approx \left(\left\{{x}\right\}×{A}\right)\wedge \left(\left\{{x}\right\}×{A}\right)\approx {A}\right)\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\approx {A}$
107 102 105 106 syl2anc ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\approx {A}$
108 domen1 ${⊢}{{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\approx {A}\to \left({{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\preccurlyeq {C}↔{A}\preccurlyeq {C}\right)$
109 107 108 syl ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left({{f}}^{-1}\left[\left\{{x}\right\}×{A}\right]\preccurlyeq {C}↔{A}\preccurlyeq {C}\right)$
110 91 109 mpbid ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to {A}\preccurlyeq {C}$
111 110 olcd ${⊢}\left({f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\wedge {x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$
112 111 ex ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)\right)$
113 112 exlimdv ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)\right)$
114 42 113 syl5bi ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({A}\setminus \left(\left({{1}^{st}↾}_{\left({A}×{A}\right)}\right)\circ {f}\right)\left[{B}\right]\ne \varnothing \to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)\right)$
115 41 114 pm2.61dne ${⊢}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$
116 115 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{B}\cup {C}\underset{1-1 onto}{⟶}{A}×{A}\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$
117 2 116 sylbi ${⊢}\left({B}\cup {C}\right)\approx \left({A}×{A}\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$
118 1 117 syl ${⊢}\left({A}×{A}\right)\approx \left({B}\cup {C}\right)\to \left({A}{\preccurlyeq }^{*}{B}\vee {A}\preccurlyeq {C}\right)$