Metamath Proof Explorer

Theorem fpwwe2lem9

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)

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

Proof

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