Metamath Proof Explorer


Theorem fpwwe2lem8

Description: Lemma for fpwwe2 . Given two well-orders <. X , R >. and <. Y , S >. of parts of A , one is an initial segment of the other. (The O C_ P hypothesis is in order to break the symmetry of X and Y .) (Contributed by Mario Carneiro, 15-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
fpwwe2.2 ( 𝜑𝐴𝑉 )
fpwwe2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
fpwwe2lem8.x ( 𝜑𝑋 𝑊 𝑅 )
fpwwe2lem8.y ( 𝜑𝑌 𝑊 𝑆 )
fpwwe2lem8.m 𝑀 = OrdIso ( 𝑅 , 𝑋 )
fpwwe2lem8.n 𝑁 = OrdIso ( 𝑆 , 𝑌 )
fpwwe2lem8.s ( 𝜑 → dom 𝑀 ⊆ dom 𝑁 )
Assertion fpwwe2lem8 ( 𝜑 → ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ( 𝜑𝐴𝑉 )
3 fpwwe2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2lem8.x ( 𝜑𝑋 𝑊 𝑅 )
5 fpwwe2lem8.y ( 𝜑𝑌 𝑊 𝑆 )
6 fpwwe2lem8.m 𝑀 = OrdIso ( 𝑅 , 𝑋 )
7 fpwwe2lem8.n 𝑁 = OrdIso ( 𝑆 , 𝑌 )
8 fpwwe2lem8.s ( 𝜑 → dom 𝑀 ⊆ dom 𝑁 )
9 1 relopabiv Rel 𝑊
10 9 brrelex1i ( 𝑋 𝑊 𝑅𝑋 ∈ V )
11 4 10 syl ( 𝜑𝑋 ∈ V )
12 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 [ ( 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
13 4 12 mpbid ( 𝜑 → ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 [ ( 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
14 13 simprld ( 𝜑𝑅 We 𝑋 )
15 6 oiiso ( ( 𝑋 ∈ V ∧ 𝑅 We 𝑋 ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
16 11 14 15 syl2anc ( 𝜑𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
17 isof1o ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → 𝑀 : dom 𝑀1-1-onto𝑋 )
18 f1ofo ( 𝑀 : dom 𝑀1-1-onto𝑋𝑀 : dom 𝑀onto𝑋 )
19 forn ( 𝑀 : dom 𝑀onto𝑋 → ran 𝑀 = 𝑋 )
20 16 17 18 19 4syl ( 𝜑 → ran 𝑀 = 𝑋 )
21 1 2 3 4 5 6 7 8 fpwwe2lem7 ( 𝜑𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
22 21 rneqd ( 𝜑 → ran 𝑀 = ran ( 𝑁 ↾ dom 𝑀 ) )
23 20 22 eqtr3d ( 𝜑𝑋 = ran ( 𝑁 ↾ dom 𝑀 ) )
24 df-ima ( 𝑁 “ dom 𝑀 ) = ran ( 𝑁 ↾ dom 𝑀 )
25 23 24 eqtr4di ( 𝜑𝑋 = ( 𝑁 “ dom 𝑀 ) )
26 imassrn ( 𝑁 “ dom 𝑀 ) ⊆ ran 𝑁
27 9 brrelex1i ( 𝑌 𝑊 𝑆𝑌 ∈ V )
28 5 27 syl ( 𝜑𝑌 ∈ V )
29 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑌 𝑊 𝑆 ↔ ( ( 𝑌𝐴𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦𝑌 [ ( 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
30 5 29 mpbid ( 𝜑 → ( ( 𝑌𝐴𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦𝑌 [ ( 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
31 30 simprld ( 𝜑𝑆 We 𝑌 )
32 7 oiiso ( ( 𝑌 ∈ V ∧ 𝑆 We 𝑌 ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
33 28 31 32 syl2anc ( 𝜑𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
34 isof1o ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → 𝑁 : dom 𝑁1-1-onto𝑌 )
35 f1ofo ( 𝑁 : dom 𝑁1-1-onto𝑌𝑁 : dom 𝑁onto𝑌 )
36 forn ( 𝑁 : dom 𝑁onto𝑌 → ran 𝑁 = 𝑌 )
37 33 34 35 36 4syl ( 𝜑 → ran 𝑁 = 𝑌 )
38 26 37 sseqtrid ( 𝜑 → ( 𝑁 “ dom 𝑀 ) ⊆ 𝑌 )
39 25 38 eqsstrd ( 𝜑𝑋𝑌 )
40 13 simplrd ( 𝜑𝑅 ⊆ ( 𝑋 × 𝑋 ) )
41 relxp Rel ( 𝑋 × 𝑋 )
42 relss ( 𝑅 ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel 𝑅 ) )
43 40 41 42 mpisyl ( 𝜑 → Rel 𝑅 )
44 relinxp Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) )
45 43 44 jctir ( 𝜑 → ( Rel 𝑅 ∧ Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )
46 40 ssbrd ( 𝜑 → ( 𝑥 𝑅 𝑦𝑥 ( 𝑋 × 𝑋 ) 𝑦 ) )
47 brxp ( 𝑥 ( 𝑋 × 𝑋 ) 𝑦 ↔ ( 𝑥𝑋𝑦𝑋 ) )
48 46 47 imbitrdi ( 𝜑 → ( 𝑥 𝑅 𝑦 → ( 𝑥𝑋𝑦𝑋 ) ) )
49 brinxp2 ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ↔ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) )
50 isocnv ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
51 33 50 syl ( 𝜑 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
52 51 adantr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
53 isof1o ( 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) → 𝑁 : 𝑌1-1-onto→ dom 𝑁 )
54 f1ofn ( 𝑁 : 𝑌1-1-onto→ dom 𝑁 𝑁 Fn 𝑌 )
55 52 53 54 3syl ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑁 Fn 𝑌 )
56 simprll ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥𝑌 )
57 simprr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 𝑆 𝑦 )
58 39 adantr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋𝑌 )
59 simprlr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦𝑋 )
60 58 59 sseldd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦𝑌 )
61 isorel ( ( 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) ∧ ( 𝑥𝑌𝑦𝑌 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( 𝑁𝑥 ) E ( 𝑁𝑦 ) ) )
62 52 56 60 61 syl12anc ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( 𝑁𝑥 ) E ( 𝑁𝑦 ) ) )
63 57 62 mpbid ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑁𝑥 ) E ( 𝑁𝑦 ) )
64 fvex ( 𝑁𝑦 ) ∈ V
65 64 epeli ( ( 𝑁𝑥 ) E ( 𝑁𝑦 ) ↔ ( 𝑁𝑥 ) ∈ ( 𝑁𝑦 ) )
66 63 65 sylib ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑁𝑥 ) ∈ ( 𝑁𝑦 ) )
67 21 adantr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
68 67 cnveqd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
69 fnfun ( 𝑁 Fn 𝑌 → Fun 𝑁 )
70 funcnvres ( Fun 𝑁 ( 𝑁 ↾ dom 𝑀 ) = ( 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
71 55 69 70 3syl ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑁 ↾ dom 𝑀 ) = ( 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
72 68 71 eqtrd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑀 = ( 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
73 72 fveq1d ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑀𝑦 ) = ( ( 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) ‘ 𝑦 ) )
74 25 adantr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
75 59 74 eleqtrd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) )
76 75 fvresd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ( 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) ‘ 𝑦 ) = ( 𝑁𝑦 ) )
77 73 76 eqtrd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑀𝑦 ) = ( 𝑁𝑦 ) )
78 isocnv ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) )
79 isof1o ( 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) → 𝑀 : 𝑋1-1-onto→ dom 𝑀 )
80 f1of ( 𝑀 : 𝑋1-1-onto→ dom 𝑀 𝑀 : 𝑋 ⟶ dom 𝑀 )
81 16 78 79 80 4syl ( 𝜑 𝑀 : 𝑋 ⟶ dom 𝑀 )
82 81 adantr ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑀 : 𝑋 ⟶ dom 𝑀 )
83 82 59 ffvelcdmd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑀𝑦 ) ∈ dom 𝑀 )
84 77 83 eqeltrrd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑁𝑦 ) ∈ dom 𝑀 )
85 6 oicl Ord dom 𝑀
86 ordtr1 ( Ord dom 𝑀 → ( ( ( 𝑁𝑥 ) ∈ ( 𝑁𝑦 ) ∧ ( 𝑁𝑦 ) ∈ dom 𝑀 ) → ( 𝑁𝑥 ) ∈ dom 𝑀 ) )
87 85 86 ax-mp ( ( ( 𝑁𝑥 ) ∈ ( 𝑁𝑦 ) ∧ ( 𝑁𝑦 ) ∈ dom 𝑀 ) → ( 𝑁𝑥 ) ∈ dom 𝑀 )
88 66 84 87 syl2anc ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑁𝑥 ) ∈ dom 𝑀 )
89 55 56 88 elpreimad ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) )
90 imacnvcnv ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 )
91 74 90 eqtr4di ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
92 89 91 eleqtrrd ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥𝑋 )
93 92 59 jca ( ( 𝜑 ∧ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑥𝑋𝑦𝑋 ) )
94 93 ex ( 𝜑 → ( ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) → ( 𝑥𝑋𝑦𝑋 ) ) )
95 49 94 biimtrid ( 𝜑 → ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 → ( 𝑥𝑋𝑦𝑋 ) ) )
96 21 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
97 96 cnveqd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
98 97 fveq1d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑀𝑥 ) = ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) )
99 97 fveq1d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑀𝑦 ) = ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) )
100 98 99 breq12d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑀𝑥 ) E ( 𝑀𝑦 ) ↔ ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
101 16 78 syl ( 𝜑 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) )
102 isorel ( ( 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝑀𝑥 ) E ( 𝑀𝑦 ) ) )
103 101 102 sylan ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝑀𝑥 ) E ( 𝑀𝑦 ) ) )
104 eqidd ( 𝜑 → ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 ) )
105 isores3 ( ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 ) ) → ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) )
106 33 8 104 105 syl3anc ( 𝜑 → ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) )
107 isocnv ( ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) → ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
108 106 107 syl ( 𝜑 ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
109 108 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
110 simprl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑥𝑋 )
111 25 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
112 110 111 eleqtrd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) )
113 simprr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑦𝑋 )
114 113 111 eleqtrd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) )
115 isorel ( ( ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) ∧ ( 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
116 109 112 114 115 syl12anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
117 100 103 116 3bitr4d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑅 𝑦𝑥 𝑆 𝑦 ) )
118 39 sselda ( ( 𝜑𝑥𝑋 ) → 𝑥𝑌 )
119 118 adantrr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 𝑥𝑌 )
120 119 113 jca ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥𝑌𝑦𝑋 ) )
121 120 biantrurd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ( 𝑥𝑌𝑦𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) )
122 121 49 bitr4di ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑆 𝑦𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
123 117 122 bitrd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝑅 𝑦𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
124 123 ex ( 𝜑 → ( ( 𝑥𝑋𝑦𝑋 ) → ( 𝑥 𝑅 𝑦𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) ) )
125 48 95 124 pm5.21ndd ( 𝜑 → ( 𝑥 𝑅 𝑦𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
126 df-br ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
127 df-br ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
128 125 126 127 3bitr3g ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )
129 128 eqrelrdv2 ( ( ( Rel 𝑅 ∧ Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∧ 𝜑 ) → 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
130 45 129 mpancom ( 𝜑𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
131 39 130 jca ( 𝜑 → ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )