Metamath Proof Explorer


Theorem fpwwe2lem5

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (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 ( 𝑆 , 𝑌 )
fpwwe2lem5.1 ( 𝜑𝐵 ∈ dom 𝑀 )
fpwwe2lem5.2 ( 𝜑𝐵 ∈ dom 𝑁 )
fpwwe2lem5.3 ( 𝜑 → ( 𝑀𝐵 ) = ( 𝑁𝐵 ) )
Assertion fpwwe2lem5 ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝐶𝑋𝐶𝑌 ∧ ( 𝑀𝐶 ) = ( 𝑁𝐶 ) ) )

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 fpwwe2lem5.1 ( 𝜑𝐵 ∈ dom 𝑀 )
9 fpwwe2lem5.2 ( 𝜑𝐵 ∈ dom 𝑁 )
10 fpwwe2lem5.3 ( 𝜑 → ( 𝑀𝐵 ) = ( 𝑁𝐵 ) )
11 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 [ ( 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
12 4 11 mpbid ( 𝜑 → ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 [ ( 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
13 12 simplrd ( 𝜑𝑅 ⊆ ( 𝑋 × 𝑋 ) )
14 13 ssbrd ( 𝜑 → ( 𝐶 𝑅 ( 𝑀𝐵 ) → 𝐶 ( 𝑋 × 𝑋 ) ( 𝑀𝐵 ) ) )
15 brxp ( 𝐶 ( 𝑋 × 𝑋 ) ( 𝑀𝐵 ) ↔ ( 𝐶𝑋 ∧ ( 𝑀𝐵 ) ∈ 𝑋 ) )
16 15 simplbi ( 𝐶 ( 𝑋 × 𝑋 ) ( 𝑀𝐵 ) → 𝐶𝑋 )
17 14 16 syl6 ( 𝜑 → ( 𝐶 𝑅 ( 𝑀𝐵 ) → 𝐶𝑋 ) )
18 17 imp ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐶𝑋 )
19 imassrn ( 𝑁𝐵 ) ⊆ ran 𝑁
20 1 relopabiv Rel 𝑊
21 20 brrelex1i ( 𝑌 𝑊 𝑆𝑌 ∈ V )
22 5 21 syl ( 𝜑𝑌 ∈ V )
23 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑌 𝑊 𝑆 ↔ ( ( 𝑌𝐴𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦𝑌 [ ( 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
24 5 23 mpbid ( 𝜑 → ( ( 𝑌𝐴𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦𝑌 [ ( 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
25 24 simprld ( 𝜑𝑆 We 𝑌 )
26 7 oiiso ( ( 𝑌 ∈ V ∧ 𝑆 We 𝑌 ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
27 22 25 26 syl2anc ( 𝜑𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
28 27 adantr ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
29 isof1o ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → 𝑁 : dom 𝑁1-1-onto𝑌 )
30 28 29 syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝑁 : dom 𝑁1-1-onto𝑌 )
31 f1ofo ( 𝑁 : dom 𝑁1-1-onto𝑌𝑁 : dom 𝑁onto𝑌 )
32 forn ( 𝑁 : dom 𝑁onto𝑌 → ran 𝑁 = 𝑌 )
33 30 31 32 3syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ran 𝑁 = 𝑌 )
34 19 33 sseqtrid ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑁𝐵 ) ⊆ 𝑌 )
35 20 brrelex1i ( 𝑋 𝑊 𝑅𝑋 ∈ V )
36 4 35 syl ( 𝜑𝑋 ∈ V )
37 12 simprld ( 𝜑𝑅 We 𝑋 )
38 6 oiiso ( ( 𝑋 ∈ V ∧ 𝑅 We 𝑋 ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
39 36 37 38 syl2anc ( 𝜑𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
40 39 adantr ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
41 isof1o ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → 𝑀 : dom 𝑀1-1-onto𝑋 )
42 40 41 syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝑀 : dom 𝑀1-1-onto𝑋 )
43 f1ocnvfv2 ( ( 𝑀 : dom 𝑀1-1-onto𝑋𝐶𝑋 ) → ( 𝑀 ‘ ( 𝑀𝐶 ) ) = 𝐶 )
44 42 18 43 syl2anc ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀 ‘ ( 𝑀𝐶 ) ) = 𝐶 )
45 simpr ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐶 𝑅 ( 𝑀𝐵 ) )
46 44 45 eqbrtrd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀 ‘ ( 𝑀𝐶 ) ) 𝑅 ( 𝑀𝐵 ) )
47 f1ocnv ( 𝑀 : dom 𝑀1-1-onto𝑋 𝑀 : 𝑋1-1-onto→ dom 𝑀 )
48 f1of ( 𝑀 : 𝑋1-1-onto→ dom 𝑀 𝑀 : 𝑋 ⟶ dom 𝑀 )
49 42 47 48 3syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝑀 : 𝑋 ⟶ dom 𝑀 )
50 49 18 ffvelrnd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐶 ) ∈ dom 𝑀 )
51 8 adantr ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐵 ∈ dom 𝑀 )
52 isorel ( ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) ∧ ( ( 𝑀𝐶 ) ∈ dom 𝑀𝐵 ∈ dom 𝑀 ) ) → ( ( 𝑀𝐶 ) E 𝐵 ↔ ( 𝑀 ‘ ( 𝑀𝐶 ) ) 𝑅 ( 𝑀𝐵 ) ) )
53 40 50 51 52 syl12anc ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( ( 𝑀𝐶 ) E 𝐵 ↔ ( 𝑀 ‘ ( 𝑀𝐶 ) ) 𝑅 ( 𝑀𝐵 ) ) )
54 46 53 mpbird ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐶 ) E 𝐵 )
55 epelg ( 𝐵 ∈ dom 𝑀 → ( ( 𝑀𝐶 ) E 𝐵 ↔ ( 𝑀𝐶 ) ∈ 𝐵 ) )
56 51 55 syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( ( 𝑀𝐶 ) E 𝐵 ↔ ( 𝑀𝐶 ) ∈ 𝐵 ) )
57 54 56 mpbid ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐶 ) ∈ 𝐵 )
58 ffn ( 𝑀 : 𝑋 ⟶ dom 𝑀 𝑀 Fn 𝑋 )
59 elpreima ( 𝑀 Fn 𝑋 → ( 𝐶 ∈ ( 𝑀𝐵 ) ↔ ( 𝐶𝑋 ∧ ( 𝑀𝐶 ) ∈ 𝐵 ) ) )
60 49 58 59 3syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝐶 ∈ ( 𝑀𝐵 ) ↔ ( 𝐶𝑋 ∧ ( 𝑀𝐶 ) ∈ 𝐵 ) ) )
61 18 57 60 mpbir2and ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐶 ∈ ( 𝑀𝐵 ) )
62 imacnvcnv ( 𝑀𝐵 ) = ( 𝑀𝐵 )
63 61 62 eleqtrdi ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐶 ∈ ( 𝑀𝐵 ) )
64 10 adantr ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐵 ) = ( 𝑁𝐵 ) )
65 64 rneqd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ran ( 𝑀𝐵 ) = ran ( 𝑁𝐵 ) )
66 df-ima ( 𝑀𝐵 ) = ran ( 𝑀𝐵 )
67 df-ima ( 𝑁𝐵 ) = ran ( 𝑁𝐵 )
68 65 66 67 3eqtr4g ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐵 ) = ( 𝑁𝐵 ) )
69 63 68 eleqtrd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐶 ∈ ( 𝑁𝐵 ) )
70 34 69 sseldd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → 𝐶𝑌 )
71 64 cnveqd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐵 ) = ( 𝑁𝐵 ) )
72 dff1o3 ( 𝑀 : dom 𝑀1-1-onto𝑋 ↔ ( 𝑀 : dom 𝑀onto𝑋 ∧ Fun 𝑀 ) )
73 72 simprbi ( 𝑀 : dom 𝑀1-1-onto𝑋 → Fun 𝑀 )
74 funcnvres ( Fun 𝑀 ( 𝑀𝐵 ) = ( 𝑀 ↾ ( 𝑀𝐵 ) ) )
75 42 73 74 3syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐵 ) = ( 𝑀 ↾ ( 𝑀𝐵 ) ) )
76 dff1o3 ( 𝑁 : dom 𝑁1-1-onto𝑌 ↔ ( 𝑁 : dom 𝑁onto𝑌 ∧ Fun 𝑁 ) )
77 76 simprbi ( 𝑁 : dom 𝑁1-1-onto𝑌 → Fun 𝑁 )
78 funcnvres ( Fun 𝑁 ( 𝑁𝐵 ) = ( 𝑁 ↾ ( 𝑁𝐵 ) ) )
79 30 77 78 3syl ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑁𝐵 ) = ( 𝑁 ↾ ( 𝑁𝐵 ) ) )
80 71 75 79 3eqtr3d ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀 ↾ ( 𝑀𝐵 ) ) = ( 𝑁 ↾ ( 𝑁𝐵 ) ) )
81 80 fveq1d ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( ( 𝑀 ↾ ( 𝑀𝐵 ) ) ‘ 𝐶 ) = ( ( 𝑁 ↾ ( 𝑁𝐵 ) ) ‘ 𝐶 ) )
82 63 fvresd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( ( 𝑀 ↾ ( 𝑀𝐵 ) ) ‘ 𝐶 ) = ( 𝑀𝐶 ) )
83 69 fvresd ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( ( 𝑁 ↾ ( 𝑁𝐵 ) ) ‘ 𝐶 ) = ( 𝑁𝐶 ) )
84 81 82 83 3eqtr3d ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝑀𝐶 ) = ( 𝑁𝐶 ) )
85 18 70 84 3jca ( ( 𝜑𝐶 𝑅 ( 𝑀𝐵 ) ) → ( 𝐶𝑋𝐶𝑌 ∧ ( 𝑀𝐶 ) = ( 𝑁𝐶 ) ) )