# Metamath Proof Explorer

## Theorem frxp

Description: A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013) (Proof shortened by Wolf Lammen, 4-Oct-2014)

Ref Expression
Hypothesis frxp.1 ${⊢}{T}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({x}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({x}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({x}\right){S}{2}^{nd}\left({y}\right)\right)\right)\right)\right\}$
Assertion frxp ${⊢}\left({R}\mathrm{Fr}{A}\wedge {S}\mathrm{Fr}{B}\right)\to {T}\mathrm{Fr}\left({A}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 frxp.1 ${⊢}{T}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({x}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({x}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({x}\right){S}{2}^{nd}\left({y}\right)\right)\right)\right)\right\}$
2 ssn0 ${⊢}\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to {A}×{B}\ne \varnothing$
3 xpnz ${⊢}\left({A}\ne \varnothing \wedge {B}\ne \varnothing \right)↔{A}×{B}\ne \varnothing$
4 3 biimpri ${⊢}{A}×{B}\ne \varnothing \to \left({A}\ne \varnothing \wedge {B}\ne \varnothing \right)$
5 4 simprd ${⊢}{A}×{B}\ne \varnothing \to {B}\ne \varnothing$
6 2 5 syl ${⊢}\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to {B}\ne \varnothing$
7 dmxp ${⊢}{B}\ne \varnothing \to \mathrm{dom}\left({A}×{B}\right)={A}$
8 dmss ${⊢}{s}\subseteq {A}×{B}\to \mathrm{dom}{s}\subseteq \mathrm{dom}\left({A}×{B}\right)$
9 sseq2 ${⊢}\mathrm{dom}\left({A}×{B}\right)={A}\to \left(\mathrm{dom}{s}\subseteq \mathrm{dom}\left({A}×{B}\right)↔\mathrm{dom}{s}\subseteq {A}\right)$
10 8 9 syl5ib ${⊢}\mathrm{dom}\left({A}×{B}\right)={A}\to \left({s}\subseteq {A}×{B}\to \mathrm{dom}{s}\subseteq {A}\right)$
11 7 10 syl ${⊢}{B}\ne \varnothing \to \left({s}\subseteq {A}×{B}\to \mathrm{dom}{s}\subseteq {A}\right)$
12 11 impcom ${⊢}\left({s}\subseteq {A}×{B}\wedge {B}\ne \varnothing \right)\to \mathrm{dom}{s}\subseteq {A}$
13 6 12 syldan ${⊢}\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \mathrm{dom}{s}\subseteq {A}$
14 relxp ${⊢}\mathrm{Rel}\left({A}×{B}\right)$
15 relss ${⊢}{s}\subseteq {A}×{B}\to \left(\mathrm{Rel}\left({A}×{B}\right)\to \mathrm{Rel}{s}\right)$
16 14 15 mpi ${⊢}{s}\subseteq {A}×{B}\to \mathrm{Rel}{s}$
17 reldm0 ${⊢}\mathrm{Rel}{s}\to \left({s}=\varnothing ↔\mathrm{dom}{s}=\varnothing \right)$
18 16 17 syl ${⊢}{s}\subseteq {A}×{B}\to \left({s}=\varnothing ↔\mathrm{dom}{s}=\varnothing \right)$
19 18 necon3bid ${⊢}{s}\subseteq {A}×{B}\to \left({s}\ne \varnothing ↔\mathrm{dom}{s}\ne \varnothing \right)$
20 19 biimpa ${⊢}\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \mathrm{dom}{s}\ne \varnothing$
21 13 20 jca ${⊢}\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left(\mathrm{dom}{s}\subseteq {A}\wedge \mathrm{dom}{s}\ne \varnothing \right)$
22 df-fr ${⊢}{R}\mathrm{Fr}{A}↔\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({v}\subseteq {A}\wedge {v}\ne \varnothing \right)\to \exists {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
23 vex ${⊢}{s}\in \mathrm{V}$
24 23 dmex ${⊢}\mathrm{dom}{s}\in \mathrm{V}$
25 sseq1 ${⊢}{v}=\mathrm{dom}{s}\to \left({v}\subseteq {A}↔\mathrm{dom}{s}\subseteq {A}\right)$
26 neeq1 ${⊢}{v}=\mathrm{dom}{s}\to \left({v}\ne \varnothing ↔\mathrm{dom}{s}\ne \varnothing \right)$
27 25 26 anbi12d ${⊢}{v}=\mathrm{dom}{s}\to \left(\left({v}\subseteq {A}\wedge {v}\ne \varnothing \right)↔\left(\mathrm{dom}{s}\subseteq {A}\wedge \mathrm{dom}{s}\ne \varnothing \right)\right)$
28 raleq ${⊢}{v}=\mathrm{dom}{s}\to \left(\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}↔\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
29 28 rexeqbi1dv ${⊢}{v}=\mathrm{dom}{s}\to \left(\exists {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}↔\exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
30 27 29 imbi12d ${⊢}{v}=\mathrm{dom}{s}\to \left(\left(\left({v}\subseteq {A}\wedge {v}\ne \varnothing \right)\to \exists {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)↔\left(\left(\mathrm{dom}{s}\subseteq {A}\wedge \mathrm{dom}{s}\ne \varnothing \right)\to \exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\right)$
31 24 30 spcv ${⊢}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({v}\subseteq {A}\wedge {v}\ne \varnothing \right)\to \exists {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left(\left(\mathrm{dom}{s}\subseteq {A}\wedge \mathrm{dom}{s}\ne \varnothing \right)\to \exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
32 22 31 sylbi ${⊢}{R}\mathrm{Fr}{A}\to \left(\left(\mathrm{dom}{s}\subseteq {A}\wedge \mathrm{dom}{s}\ne \varnothing \right)\to \exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
33 21 32 syl5 ${⊢}{R}\mathrm{Fr}{A}\to \left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
34 33 adantr ${⊢}\left({R}\mathrm{Fr}{A}\wedge {S}\mathrm{Fr}{B}\right)\to \left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)$
35 imassrn ${⊢}{s}\left[\left\{{a}\right\}\right]\subseteq \mathrm{ran}{s}$
36 xpeq0 ${⊢}{A}×{B}=\varnothing ↔\left({A}=\varnothing \vee {B}=\varnothing \right)$
37 36 biimpri ${⊢}\left({A}=\varnothing \vee {B}=\varnothing \right)\to {A}×{B}=\varnothing$
38 37 orcs ${⊢}{A}=\varnothing \to {A}×{B}=\varnothing$
39 sseq2 ${⊢}{A}×{B}=\varnothing \to \left({s}\subseteq {A}×{B}↔{s}\subseteq \varnothing \right)$
40 ss0 ${⊢}{s}\subseteq \varnothing \to {s}=\varnothing$
41 39 40 syl6bi ${⊢}{A}×{B}=\varnothing \to \left({s}\subseteq {A}×{B}\to {s}=\varnothing \right)$
42 38 41 syl ${⊢}{A}=\varnothing \to \left({s}\subseteq {A}×{B}\to {s}=\varnothing \right)$
43 rneq ${⊢}{s}=\varnothing \to \mathrm{ran}{s}=\mathrm{ran}\varnothing$
44 rn0 ${⊢}\mathrm{ran}\varnothing =\varnothing$
45 0ss ${⊢}\varnothing \subseteq {B}$
46 44 45 eqsstri ${⊢}\mathrm{ran}\varnothing \subseteq {B}$
47 43 46 eqsstrdi ${⊢}{s}=\varnothing \to \mathrm{ran}{s}\subseteq {B}$
48 42 47 syl6 ${⊢}{A}=\varnothing \to \left({s}\subseteq {A}×{B}\to \mathrm{ran}{s}\subseteq {B}\right)$
49 rnxp ${⊢}{A}\ne \varnothing \to \mathrm{ran}\left({A}×{B}\right)={B}$
50 rnss ${⊢}{s}\subseteq {A}×{B}\to \mathrm{ran}{s}\subseteq \mathrm{ran}\left({A}×{B}\right)$
51 sseq2 ${⊢}\mathrm{ran}\left({A}×{B}\right)={B}\to \left(\mathrm{ran}{s}\subseteq \mathrm{ran}\left({A}×{B}\right)↔\mathrm{ran}{s}\subseteq {B}\right)$
52 50 51 syl5ib ${⊢}\mathrm{ran}\left({A}×{B}\right)={B}\to \left({s}\subseteq {A}×{B}\to \mathrm{ran}{s}\subseteq {B}\right)$
53 49 52 syl ${⊢}{A}\ne \varnothing \to \left({s}\subseteq {A}×{B}\to \mathrm{ran}{s}\subseteq {B}\right)$
54 48 53 pm2.61ine ${⊢}{s}\subseteq {A}×{B}\to \mathrm{ran}{s}\subseteq {B}$
55 35 54 sstrid ${⊢}{s}\subseteq {A}×{B}\to {s}\left[\left\{{a}\right\}\right]\subseteq {B}$
56 vex ${⊢}{a}\in \mathrm{V}$
57 56 eldm ${⊢}{a}\in \mathrm{dom}{s}↔\exists {b}\phantom{\rule{.4em}{0ex}}{a}{s}{b}$
58 vex ${⊢}{b}\in \mathrm{V}$
59 56 58 elimasn ${⊢}{b}\in {s}\left[\left\{{a}\right\}\right]↔⟨{a},{b}⟩\in {s}$
60 df-br ${⊢}{a}{s}{b}↔⟨{a},{b}⟩\in {s}$
61 59 60 bitr4i ${⊢}{b}\in {s}\left[\left\{{a}\right\}\right]↔{a}{s}{b}$
62 ne0i ${⊢}{b}\in {s}\left[\left\{{a}\right\}\right]\to {s}\left[\left\{{a}\right\}\right]\ne \varnothing$
63 61 62 sylbir ${⊢}{a}{s}{b}\to {s}\left[\left\{{a}\right\}\right]\ne \varnothing$
64 63 exlimiv ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}{a}{s}{b}\to {s}\left[\left\{{a}\right\}\right]\ne \varnothing$
65 57 64 sylbi ${⊢}{a}\in \mathrm{dom}{s}\to {s}\left[\left\{{a}\right\}\right]\ne \varnothing$
66 df-fr ${⊢}{S}\mathrm{Fr}{B}↔\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({v}\subseteq {B}\wedge {v}\ne \varnothing \right)\to \exists {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {d}\in {v}\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)$
67 23 imaex ${⊢}{s}\left[\left\{{a}\right\}\right]\in \mathrm{V}$
68 sseq1 ${⊢}{v}={s}\left[\left\{{a}\right\}\right]\to \left({v}\subseteq {B}↔{s}\left[\left\{{a}\right\}\right]\subseteq {B}\right)$
69 neeq1 ${⊢}{v}={s}\left[\left\{{a}\right\}\right]\to \left({v}\ne \varnothing ↔{s}\left[\left\{{a}\right\}\right]\ne \varnothing \right)$
70 68 69 anbi12d ${⊢}{v}={s}\left[\left\{{a}\right\}\right]\to \left(\left({v}\subseteq {B}\wedge {v}\ne \varnothing \right)↔\left({s}\left[\left\{{a}\right\}\right]\subseteq {B}\wedge {s}\left[\left\{{a}\right\}\right]\ne \varnothing \right)\right)$
71 raleq ${⊢}{v}={s}\left[\left\{{a}\right\}\right]\to \left(\forall {d}\in {v}\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}↔\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)$
72 71 rexeqbi1dv ${⊢}{v}={s}\left[\left\{{a}\right\}\right]\to \left(\exists {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {d}\in {v}\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}↔\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)$
73 70 72 imbi12d ${⊢}{v}={s}\left[\left\{{a}\right\}\right]\to \left(\left(\left({v}\subseteq {B}\wedge {v}\ne \varnothing \right)\to \exists {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {d}\in {v}\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)↔\left(\left({s}\left[\left\{{a}\right\}\right]\subseteq {B}\wedge {s}\left[\left\{{a}\right\}\right]\ne \varnothing \right)\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\right)$
74 67 73 spcv ${⊢}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({v}\subseteq {B}\wedge {v}\ne \varnothing \right)\to \exists {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {d}\in {v}\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left(\left({s}\left[\left\{{a}\right\}\right]\subseteq {B}\wedge {s}\left[\left\{{a}\right\}\right]\ne \varnothing \right)\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)$
75 66 74 sylbi ${⊢}{S}\mathrm{Fr}{B}\to \left(\left({s}\left[\left\{{a}\right\}\right]\subseteq {B}\wedge {s}\left[\left\{{a}\right\}\right]\ne \varnothing \right)\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)$
76 55 65 75 syl2ani ${⊢}{S}\mathrm{Fr}{B}\to \left(\left({s}\subseteq {A}×{B}\wedge {a}\in \mathrm{dom}{s}\right)\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)$
77 1stdm ${⊢}\left(\mathrm{Rel}{s}\wedge {w}\in {s}\right)\to {1}^{st}\left({w}\right)\in \mathrm{dom}{s}$
78 breq1 ${⊢}{c}={1}^{st}\left({w}\right)\to \left({c}{R}{a}↔{1}^{st}\left({w}\right){R}{a}\right)$
79 78 notbid ${⊢}{c}={1}^{st}\left({w}\right)\to \left(¬{c}{R}{a}↔¬{1}^{st}\left({w}\right){R}{a}\right)$
80 79 rspccv ${⊢}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \left({1}^{st}\left({w}\right)\in \mathrm{dom}{s}\to ¬{1}^{st}\left({w}\right){R}{a}\right)$
81 77 80 syl5 ${⊢}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \left(\left(\mathrm{Rel}{s}\wedge {w}\in {s}\right)\to ¬{1}^{st}\left({w}\right){R}{a}\right)$
82 81 expd ${⊢}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \left(\mathrm{Rel}{s}\to \left({w}\in {s}\to ¬{1}^{st}\left({w}\right){R}{a}\right)\right)$
83 82 impcom ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left({w}\in {s}\to ¬{1}^{st}\left({w}\right){R}{a}\right)$
84 83 adantr ${⊢}\left(\left(\mathrm{Rel}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to ¬{1}^{st}\left({w}\right){R}{a}\right)$
85 elrel ${⊢}\left(\mathrm{Rel}{s}\wedge {w}\in {s}\right)\to \exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}{w}=⟨{t},{u}⟩$
86 85 ex ${⊢}\mathrm{Rel}{s}\to \left({w}\in {s}\to \exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}{w}=⟨{t},{u}⟩\right)$
87 86 adantr ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}{w}=⟨{t},{u}⟩\right)$
88 vex ${⊢}{u}\in \mathrm{V}$
89 56 88 elimasn ${⊢}{u}\in {s}\left[\left\{{a}\right\}\right]↔⟨{a},{u}⟩\in {s}$
90 breq1 ${⊢}{d}={u}\to \left({d}{S}{b}↔{u}{S}{b}\right)$
91 90 notbid ${⊢}{d}={u}\to \left(¬{d}{S}{b}↔¬{u}{S}{b}\right)$
92 91 rspccv ${⊢}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \left({u}\in {s}\left[\left\{{a}\right\}\right]\to ¬{u}{S}{b}\right)$
93 89 92 syl5bir ${⊢}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \left(⟨{a},{u}⟩\in {s}\to ¬{u}{S}{b}\right)$
94 93 adantl ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left(⟨{a},{u}⟩\in {s}\to ¬{u}{S}{b}\right)$
95 opeq1 ${⊢}{t}={a}\to ⟨{t},{u}⟩=⟨{a},{u}⟩$
96 95 eleq1d ${⊢}{t}={a}\to \left(⟨{t},{u}⟩\in {s}↔⟨{a},{u}⟩\in {s}\right)$
97 96 imbi1d ${⊢}{t}={a}\to \left(\left(⟨{t},{u}⟩\in {s}\to ¬{u}{S}{b}\right)↔\left(⟨{a},{u}⟩\in {s}\to ¬{u}{S}{b}\right)\right)$
98 94 97 syl5ibr ${⊢}{t}={a}\to \left(\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left(⟨{t},{u}⟩\in {s}\to ¬{u}{S}{b}\right)\right)$
99 98 com3l ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left(⟨{t},{u}⟩\in {s}\to \left({t}={a}\to ¬{u}{S}{b}\right)\right)$
100 eleq1 ${⊢}{w}=⟨{t},{u}⟩\to \left({w}\in {s}↔⟨{t},{u}⟩\in {s}\right)$
101 vex ${⊢}{t}\in \mathrm{V}$
102 101 88 op1std ${⊢}{w}=⟨{t},{u}⟩\to {1}^{st}\left({w}\right)={t}$
103 102 eqeq1d ${⊢}{w}=⟨{t},{u}⟩\to \left({1}^{st}\left({w}\right)={a}↔{t}={a}\right)$
104 101 88 op2ndd ${⊢}{w}=⟨{t},{u}⟩\to {2}^{nd}\left({w}\right)={u}$
105 104 breq1d ${⊢}{w}=⟨{t},{u}⟩\to \left({2}^{nd}\left({w}\right){S}{b}↔{u}{S}{b}\right)$
106 105 notbid ${⊢}{w}=⟨{t},{u}⟩\to \left(¬{2}^{nd}\left({w}\right){S}{b}↔¬{u}{S}{b}\right)$
107 103 106 imbi12d ${⊢}{w}=⟨{t},{u}⟩\to \left(\left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)↔\left({t}={a}\to ¬{u}{S}{b}\right)\right)$
108 100 107 imbi12d ${⊢}{w}=⟨{t},{u}⟩\to \left(\left({w}\in {s}\to \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)↔\left(⟨{t},{u}⟩\in {s}\to \left({t}={a}\to ¬{u}{S}{b}\right)\right)\right)$
109 99 108 syl5ibr ${⊢}{w}=⟨{t},{u}⟩\to \left(\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
110 109 exlimivv ${⊢}\exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}{w}=⟨{t},{u}⟩\to \left(\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
111 110 com3l ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}{w}=⟨{t},{u}⟩\to \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
112 87 111 mpdd ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)$
113 112 adantlr ${⊢}\left(\left(\mathrm{Rel}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)$
114 84 113 jcad ${⊢}\left(\left(\mathrm{Rel}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \left({w}\in {s}\to \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
115 114 ralrimiv ${⊢}\left(\left(\mathrm{Rel}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\wedge \forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\right)\to \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)$
116 115 ex ${⊢}\left(\mathrm{Rel}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left(\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
117 16 116 sylan ${⊢}\left({s}\subseteq {A}×{B}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left(\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
118 olc ${⊢}\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\to \left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
119 118 ralimi ${⊢}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\to \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
120 117 119 syl6 ${⊢}\left({s}\subseteq {A}×{B}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left(\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)\right)$
121 ianor ${⊢}¬\left(\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)↔\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee ¬\left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
122 vex ${⊢}{w}\in \mathrm{V}$
123 opex ${⊢}⟨{a},{b}⟩\in \mathrm{V}$
124 eleq1 ${⊢}{x}={w}\to \left({x}\in \left({A}×{B}\right)↔{w}\in \left({A}×{B}\right)\right)$
125 124 anbi1d ${⊢}{x}={w}\to \left(\left({x}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)↔\left({w}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)\right)$
126 fveq2 ${⊢}{x}={w}\to {1}^{st}\left({x}\right)={1}^{st}\left({w}\right)$
127 126 breq1d ${⊢}{x}={w}\to \left({1}^{st}\left({x}\right){R}{1}^{st}\left({y}\right)↔{1}^{st}\left({w}\right){R}{1}^{st}\left({y}\right)\right)$
128 126 eqeq1d ${⊢}{x}={w}\to \left({1}^{st}\left({x}\right)={1}^{st}\left({y}\right)↔{1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\right)$
129 fveq2 ${⊢}{x}={w}\to {2}^{nd}\left({x}\right)={2}^{nd}\left({w}\right)$
130 129 breq1d ${⊢}{x}={w}\to \left({2}^{nd}\left({x}\right){S}{2}^{nd}\left({y}\right)↔{2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)$
131 128 130 anbi12d ${⊢}{x}={w}\to \left(\left({1}^{st}\left({x}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({x}\right){S}{2}^{nd}\left({y}\right)\right)↔\left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)\right)$
132 127 131 orbi12d ${⊢}{x}={w}\to \left(\left({1}^{st}\left({x}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({x}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({x}\right){S}{2}^{nd}\left({y}\right)\right)\right)↔\left({1}^{st}\left({w}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)\right)\right)$
133 125 132 anbi12d ${⊢}{x}={w}\to \left(\left(\left({x}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({x}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({x}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({x}\right){S}{2}^{nd}\left({y}\right)\right)\right)\right)↔\left(\left({w}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({w}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)\right)\right)\right)$
134 eleq1 ${⊢}{y}=⟨{a},{b}⟩\to \left({y}\in \left({A}×{B}\right)↔⟨{a},{b}⟩\in \left({A}×{B}\right)\right)$
135 134 anbi2d ${⊢}{y}=⟨{a},{b}⟩\to \left(\left({w}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)↔\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\right)$
136 56 58 op1std ${⊢}{y}=⟨{a},{b}⟩\to {1}^{st}\left({y}\right)={a}$
137 136 breq2d ${⊢}{y}=⟨{a},{b}⟩\to \left({1}^{st}\left({w}\right){R}{1}^{st}\left({y}\right)↔{1}^{st}\left({w}\right){R}{a}\right)$
138 136 eqeq2d ${⊢}{y}=⟨{a},{b}⟩\to \left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)↔{1}^{st}\left({w}\right)={a}\right)$
139 56 58 op2ndd ${⊢}{y}=⟨{a},{b}⟩\to {2}^{nd}\left({y}\right)={b}$
140 139 breq2d ${⊢}{y}=⟨{a},{b}⟩\to \left({2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)↔{2}^{nd}\left({w}\right){S}{b}\right)$
141 138 140 anbi12d ${⊢}{y}=⟨{a},{b}⟩\to \left(\left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)↔\left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)$
142 137 141 orbi12d ${⊢}{y}=⟨{a},{b}⟩\to \left(\left({1}^{st}\left({w}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)\right)↔\left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
143 135 142 anbi12d ${⊢}{y}=⟨{a},{b}⟩\to \left(\left(\left({w}\in \left({A}×{B}\right)\wedge {y}\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({w}\right){R}{1}^{st}\left({y}\right)\vee \left({1}^{st}\left({w}\right)={1}^{st}\left({y}\right)\wedge {2}^{nd}\left({w}\right){S}{2}^{nd}\left({y}\right)\right)\right)\right)↔\left(\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)\right)$
144 122 123 133 143 1 brab ${⊢}{w}{T}⟨{a},{b}⟩↔\left(\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\wedge \left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
145 121 144 xchnxbir ${⊢}¬{w}{T}⟨{a},{b}⟩↔\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee ¬\left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
146 ioran ${⊢}¬\left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)↔\left(¬{1}^{st}\left({w}\right){R}{a}\wedge ¬\left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)$
147 ianor ${⊢}¬\left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)↔\left(¬{1}^{st}\left({w}\right)={a}\vee ¬{2}^{nd}\left({w}\right){S}{b}\right)$
148 pm4.62 ${⊢}\left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)↔\left(¬{1}^{st}\left({w}\right)={a}\vee ¬{2}^{nd}\left({w}\right){S}{b}\right)$
149 147 148 bitr4i ${⊢}¬\left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)↔\left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)$
150 149 anbi2i ${⊢}\left(¬{1}^{st}\left({w}\right){R}{a}\wedge ¬\left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)↔\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)$
151 146 150 bitri ${⊢}¬\left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)↔\left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)$
152 151 orbi2i ${⊢}\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee ¬\left({1}^{st}\left({w}\right){R}{a}\vee \left({1}^{st}\left({w}\right)={a}\wedge {2}^{nd}\left({w}\right){S}{b}\right)\right)\right)↔\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
153 145 152 bitri ${⊢}¬{w}{T}⟨{a},{b}⟩↔\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
154 153 ralbii ${⊢}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩↔\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}\left(¬\left({w}\in \left({A}×{B}\right)\wedge ⟨{a},{b}⟩\in \left({A}×{B}\right)\right)\vee \left(¬{1}^{st}\left({w}\right){R}{a}\wedge \left({1}^{st}\left({w}\right)={a}\to ¬{2}^{nd}\left({w}\right){S}{b}\right)\right)\right)$
155 120 154 syl6ibr ${⊢}\left({s}\subseteq {A}×{B}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left(\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
156 155 reximdv ${⊢}\left({s}\subseteq {A}×{B}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \left(\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
157 156 ex ${⊢}{s}\subseteq {A}×{B}\to \left(\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \left(\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)$
158 157 com23 ${⊢}{s}\subseteq {A}×{B}\to \left(\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \left(\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)$
159 158 adantr ${⊢}\left({s}\subseteq {A}×{B}\wedge {a}\in \mathrm{dom}{s}\right)\to \left(\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {d}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}¬{d}{S}{b}\to \left(\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)$
160 76 159 sylcom ${⊢}{S}\mathrm{Fr}{B}\to \left(\left({s}\subseteq {A}×{B}\wedge {a}\in \mathrm{dom}{s}\right)\to \left(\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)$
161 160 impl ${⊢}\left(\left({S}\mathrm{Fr}{B}\wedge {s}\subseteq {A}×{B}\right)\wedge {a}\in \mathrm{dom}{s}\right)\to \left(\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
162 161 expimpd ${⊢}\left({S}\mathrm{Fr}{B}\wedge {s}\subseteq {A}×{B}\right)\to \left(\left({a}\in \mathrm{dom}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
163 162 3adant3 ${⊢}\left({S}\mathrm{Fr}{B}\wedge {s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left(\left({a}\in \mathrm{dom}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
164 resss ${⊢}{{s}↾}_{\left\{{a}\right\}}\subseteq {s}$
165 df-rex ${⊢}\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩↔\exists {b}\phantom{\rule{.4em}{0ex}}\left({b}\in {s}\left[\left\{{a}\right\}\right]\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
166 eqid ${⊢}⟨{a},{b}⟩=⟨{a},{b}⟩$
167 eqeq1 ${⊢}{z}=⟨{a},{b}⟩\to \left({z}=⟨{a},{b}⟩↔⟨{a},{b}⟩=⟨{a},{b}⟩\right)$
168 breq2 ${⊢}{z}=⟨{a},{b}⟩\to \left({w}{T}{z}↔{w}{T}⟨{a},{b}⟩\right)$
169 168 notbid ${⊢}{z}=⟨{a},{b}⟩\to \left(¬{w}{T}{z}↔¬{w}{T}⟨{a},{b}⟩\right)$
170 169 ralbidv ${⊢}{z}=⟨{a},{b}⟩\to \left(\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}↔\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)$
171 170 anbi2d ${⊢}{z}=⟨{a},{b}⟩\to \left(\left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)$
172 167 171 anbi12d ${⊢}{z}=⟨{a},{b}⟩\to \left(\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)↔\left(⟨{a},{b}⟩=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)\right)$
173 123 172 spcev ${⊢}\left(⟨{a},{b}⟩=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
174 166 173 mpan ${⊢}\left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
175 59 174 sylanb ${⊢}\left({b}\in {s}\left[\left\{{a}\right\}\right]\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
176 175 eximi ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\left({b}\in {s}\left[\left\{{a}\right\}\right]\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\right)\to \exists {b}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
177 165 176 sylbi ${⊢}\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\to \exists {b}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
178 excom ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
179 177 178 sylib ${⊢}\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\to \exists {z}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
180 df-rex ${⊢}\exists {z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
181 56 elsnres ${⊢}{z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)↔\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge ⟨{a},{b}⟩\in {s}\right)$
182 181 anbi1i ${⊢}\left({z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\left(\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge ⟨{a},{b}⟩\in {s}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
183 19.41v ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\left(\left({z}=⟨{a},{b}⟩\wedge ⟨{a},{b}⟩\in {s}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\left(\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge ⟨{a},{b}⟩\in {s}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
184 anass ${⊢}\left(\left({z}=⟨{a},{b}⟩\wedge ⟨{a},{b}⟩\in {s}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
185 184 exbii ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}\left(\left({z}=⟨{a},{b}⟩\wedge ⟨{a},{b}⟩\in {s}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
186 182 183 185 3bitr2i ${⊢}\left({z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
187 186 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
188 180 187 bitri ${⊢}\exists {z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{a},{b}⟩\wedge \left(⟨{a},{b}⟩\in {s}\wedge \forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
189 179 188 sylibr ${⊢}\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\to \exists {z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}$
190 ssrexv ${⊢}{{s}↾}_{\left\{{a}\right\}}\subseteq {s}\to \left(\exists {z}\in \left({{s}↾}_{\left\{{a}\right\}}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
191 164 189 190 mpsyl ${⊢}\exists {b}\in {s}\left[\left\{{a}\right\}\right]\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}⟨{a},{b}⟩\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}$
192 163 191 syl6 ${⊢}\left({S}\mathrm{Fr}{B}\wedge {s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left(\left({a}\in \mathrm{dom}{s}\wedge \forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\right)\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
193 192 expd ${⊢}\left({S}\mathrm{Fr}{B}\wedge {s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left({a}\in \mathrm{dom}{s}\to \left(\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
194 193 rexlimdv ${⊢}\left({S}\mathrm{Fr}{B}\wedge {s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left(\exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
195 194 3expib ${⊢}{S}\mathrm{Fr}{B}\to \left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left(\exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
196 195 adantl ${⊢}\left({R}\mathrm{Fr}{A}\wedge {S}\mathrm{Fr}{B}\right)\to \left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \left(\exists {a}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}\forall {c}\in \mathrm{dom}{s}\phantom{\rule{.4em}{0ex}}¬{c}{R}{a}\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)\right)$
197 34 196 mpdd ${⊢}\left({R}\mathrm{Fr}{A}\wedge {S}\mathrm{Fr}{B}\right)\to \left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
198 197 alrimiv ${⊢}\left({R}\mathrm{Fr}{A}\wedge {S}\mathrm{Fr}{B}\right)\to \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
199 df-fr ${⊢}{T}\mathrm{Fr}\left({A}×{B}\right)↔\forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}×{B}\wedge {s}\ne \varnothing \right)\to \exists {z}\in {s}\phantom{\rule{.4em}{0ex}}\forall {w}\in {s}\phantom{\rule{.4em}{0ex}}¬{w}{T}{z}\right)$
200 198 199 sylibr ${⊢}\left({R}\mathrm{Fr}{A}\wedge {S}\mathrm{Fr}{B}\right)\to {T}\mathrm{Fr}\left({A}×{B}\right)$