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 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 fpwwe2lem7 ⊢ ( 𝜑 → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
23 22 rneqd ⊢ ( 𝜑 → ran 𝑀 = ran ( 𝑁 ↾ dom 𝑀 ) )
24 21 23 eqtr3d ⊢ ( 𝜑 → 𝑋 = ran ( 𝑁 ↾ dom 𝑀 ) )
25 df-ima ⊢ ( 𝑁 “ dom 𝑀 ) = ran ( 𝑁 ↾ dom 𝑀 )
26 24 25 eqtr4di ⊢ ( 𝜑 → 𝑋 = ( 𝑁 “ 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 imbitrdi ⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
51 brinxp2 ⊢ ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) )
52 isocnv ⊢ ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
53 34 52 syl ⊢ ( 𝜑 → ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
55 isof1o ⊢ ( ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) → ◡ 𝑁 : 𝑌 –1-1-onto→ dom 𝑁 )
56 f1ofn ⊢ ( ◡ 𝑁 : 𝑌 –1-1-onto→ dom 𝑁 → ◡ 𝑁 Fn 𝑌 )
57 54 55 56 3syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ◡ 𝑁 Fn 𝑌 )
58 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ 𝑌 )
59 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 𝑆 𝑦 )
60 41 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 ⊆ 𝑌 )
61 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦 ∈ 𝑋 )
62 60 61 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦 ∈ 𝑌 )
63 isorel ⊢ ( ( ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ◡ 𝑁 ‘ 𝑥 ) E ( ◡ 𝑁 ‘ 𝑦 ) ) )
64 54 58 62 63 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ◡ 𝑁 ‘ 𝑥 ) E ( ◡ 𝑁 ‘ 𝑦 ) ) )
65 59 64 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ◡ 𝑁 ‘ 𝑥 ) E ( ◡ 𝑁 ‘ 𝑦 ) )
66 fvex ⊢ ( ◡ 𝑁 ‘ 𝑦 ) ∈ V
67 66 epeli ⊢ ( ( ◡ 𝑁 ‘ 𝑥 ) E ( ◡ 𝑁 ‘ 𝑦 ) ↔ ( ◡ 𝑁 ‘ 𝑥 ) ∈ ( ◡ 𝑁 ‘ 𝑦 ) )
68 65 67 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ◡ 𝑁 ‘ 𝑥 ) ∈ ( ◡ 𝑁 ‘ 𝑦 ) )
69 22 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
70 69 cnveqd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ◡ 𝑀 = ◡ ( 𝑁 ↾ dom 𝑀 ) )
71 fnfun ⊢ ( ◡ 𝑁 Fn 𝑌 → Fun ◡ 𝑁 )
72 funcnvres ⊢ ( Fun ◡ 𝑁 → ◡ ( 𝑁 ↾ dom 𝑀 ) = ( ◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
73 57 71 72 3syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ◡ ( 𝑁 ↾ dom 𝑀 ) = ( ◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
74 70 73 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ◡ 𝑀 = ( ◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
75 74 fveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ◡ 𝑀 ‘ 𝑦 ) = ( ( ◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) ‘ 𝑦 ) )
76 26 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
77 61 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 61 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ◡ 𝑀 ‘ 𝑦 ) ∈ 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 68 87 90 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ◡ 𝑁 ‘ 𝑥 ) ∈ dom 𝑀 )
92 57 58 91 elpreimad ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ ( ◡ ◡ 𝑁 “ dom 𝑀 ) )
93 imacnvcnv ⊢ ( ◡ ◡ 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 )
94 76 93 eqtr4di ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 = ( ◡ ◡ 𝑁 “ dom 𝑀 ) )
95 92 94 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ 𝑋 )
96 95 61 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
97 96 ex ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
98 51 97 biimtrid ⊢ ( 𝜑 → ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
99 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
100 99 cnveqd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ◡ 𝑀 = ◡ ( 𝑁 ↾ dom 𝑀 ) )
101 100 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ◡ 𝑀 ‘ 𝑥 ) = ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) )
102 100 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ◡ 𝑀 ‘ 𝑦 ) = ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) )
103 101 102 breq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ◡ 𝑀 ‘ 𝑥 ) E ( ◡ 𝑀 ‘ 𝑦 ) ↔ ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
104 isorel ⊢ ( ( ◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ◡ 𝑀 ‘ 𝑥 ) E ( ◡ 𝑀 ‘ 𝑦 ) ) )
105 81 104 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ◡ 𝑀 ‘ 𝑥 ) E ( ◡ 𝑀 ‘ 𝑦 ) ) )
106 eqidd ⊢ ( 𝜑 → ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 ) )
107 isores3 ⊢ ( ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 ) ) → ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) )
108 34 8 106 107 syl3anc ⊢ ( 𝜑 → ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) )
109 isocnv ⊢ ( ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) → ◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
110 108 109 syl ⊢ ( 𝜑 → ◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
112 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
113 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
114 112 113 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) )
115 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
116 115 113 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) )
117 isorel ⊢ ( ( ◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) ∧ ( 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
118 111 114 116 117 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
119 103 105 118 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑆 𝑦 ) )
120 41 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑌 )
121 120 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑌 )
122 121 115 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) )
123 122 biantrurd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) )
124 123 51 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
125 119 124 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
126 125 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) ) )
127 50 98 126 pm5.21ndd ⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
128 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
129 df-br ⊢ ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
130 127 128 129 3bitr3g ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )
131 130 eqrelrdv2 ⊢ ( ( ( Rel 𝑅 ∧ Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∧ 𝜑 ) → 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
132 47 131 mpancom ⊢ ( 𝜑 → 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
133 41 132 jca ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )