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 ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )