This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wemapwe

Description: Construct lexicographic order on a function space based on a reverse well-ordering of the indices and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses wemapwe.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
wemapwe.u ⊢ 𝑈 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
wemapwe.2 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
wemapwe.3 ⊢ ( 𝜑 → 𝑆 We 𝐵 )
wemapwe.4 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
wemapwe.5 ⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
wemapwe.6 ⊢ 𝐺 = OrdIso ( 𝑆 , 𝐵 )
wemapwe.7 ⊢ 𝑍 = ( 𝐺 ‘ ∅ )
Assertion wemapwe ( 𝜑 → 𝑇 We 𝑈 )

Proof

Step Hyp Ref Expression
1 wemapwe.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
2 wemapwe.u ⊢ 𝑈 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
3 wemapwe.2 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
4 wemapwe.3 ⊢ ( 𝜑 → 𝑆 We 𝐵 )
5 wemapwe.4 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
6 wemapwe.5 ⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
7 wemapwe.6 ⊢ 𝐺 = OrdIso ( 𝑆 , 𝐵 )
8 wemapwe.7 ⊢ 𝑍 = ( 𝐺 ‘ ∅ )
9 eqid ⊢ { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) } = { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) }
10 eqid ⊢ ( ◡ 𝐺 ‘ 𝑍 ) = ( ◡ 𝐺 ‘ 𝑍 )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐴 ∈ V )
12 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝑅 We 𝐴 )
13 6 oiiso ⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
14 11 12 13 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
15 isof1o ⊢ ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
16 14 15 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐵 ∈ V )
18 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝑆 We 𝐵 )
19 7 oiiso ⊢ ( ( 𝐵 ∈ V ∧ 𝑆 We 𝐵 ) → 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) )
20 17 18 19 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) )
21 isof1o ⊢ ( 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) → 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 )
22 f1ocnv ⊢ ( 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐵 –1-1-onto→ dom 𝐺 )
23 20 21 22 3syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ◡ 𝐺 : 𝐵 –1-1-onto→ dom 𝐺 )
24 6 oiexg ⊢ ( 𝐴 ∈ V → 𝐹 ∈ V )
25 24 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐹 ∈ V )
26 25 dmexd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom 𝐹 ∈ V )
27 7 oiexg ⊢ ( 𝐵 ∈ V → 𝐺 ∈ V )
28 27 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐺 ∈ V )
29 28 dmexd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom 𝐺 ∈ V )
30 20 21 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 )
31 f1ofo ⊢ ( 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 → 𝐺 : dom 𝐺 –onto→ 𝐵 )
32 forn ⊢ ( 𝐺 : dom 𝐺 –onto→ 𝐵 → ran 𝐺 = 𝐵 )
33 30 31 32 3syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ran 𝐺 = 𝐵 )
34 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝐵 ≠ ∅ )
35 33 34 eqnetrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ran 𝐺 ≠ ∅ )
36 dm0rn0 ⊢ ( dom 𝐺 = ∅ ↔ ran 𝐺 = ∅ )
37 36 necon3bii ⊢ ( dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅ )
38 35 37 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom 𝐺 ≠ ∅ )
39 7 oicl ⊢ Ord dom 𝐺
40 ord0eln0 ⊢ ( Ord dom 𝐺 → ( ∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅ ) )
41 39 40 ax-mp ⊢ ( ∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅ )
42 38 41 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ∅ ∈ dom 𝐺 )
43 7 oif ⊢ 𝐺 : dom 𝐺 ⟶ 𝐵
44 43 ffvelcdmi ⊢ ( ∅ ∈ dom 𝐺 → ( 𝐺 ‘ ∅ ) ∈ 𝐵 )
45 42 44 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝐺 ‘ ∅ ) ∈ 𝐵 )
46 8 45 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝑍 ∈ 𝐵 )
47 2 9 10 16 23 11 17 26 29 46 mapfien ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑈 –1-1-onto→ { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) } )
48 eqid ⊢ { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ∅ } = { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ∅ }
49 7 oion ⊢ ( 𝐵 ∈ V → dom 𝐺 ∈ On )
50 49 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom 𝐺 ∈ On )
51 6 oion ⊢ ( 𝐴 ∈ V → dom 𝐹 ∈ On )
52 51 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom 𝐹 ∈ On )
53 48 50 52 cantnfdm ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom ( dom 𝐺 CNF dom 𝐹 ) = { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ∅ } )
54 8 fveq2i ⊢ ( ◡ 𝐺 ‘ 𝑍 ) = ( ◡ 𝐺 ‘ ( 𝐺 ‘ ∅ ) )
55 f1ocnvfv1 ⊢ ( ( 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 ∧ ∅ ∈ dom 𝐺 ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ ∅ ) ) = ∅ )
56 30 42 55 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ ∅ ) ) = ∅ )
57 54 56 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ◡ 𝐺 ‘ 𝑍 ) = ∅ )
58 57 breq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) ↔ 𝑥 finSupp ∅ ) )
59 58 rabbidv ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) } = { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ∅ } )
60 53 59 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → dom ( dom 𝐺 CNF dom 𝐹 ) = { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) } )
61 60 f1oeq3d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑈 –1-1-onto→ dom ( dom 𝐺 CNF dom 𝐹 ) ↔ ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑈 –1-1-onto→ { 𝑥 ∈ ( dom 𝐺 ↑m dom 𝐹 ) ∣ 𝑥 finSupp ( ◡ 𝐺 ‘ 𝑍 ) } ) )
62 47 61 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑈 –1-1-onto→ dom ( dom 𝐺 CNF dom 𝐹 ) )
63 eqid ⊢ dom ( dom 𝐺 CNF dom 𝐹 ) = dom ( dom 𝐺 CNF dom 𝐹 )
64 eqid ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) }
65 63 50 52 64 oemapwe ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } We dom ( dom 𝐺 CNF dom 𝐹 ) ∧ dom OrdIso ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } , dom ( dom 𝐺 CNF dom 𝐹 ) ) = ( dom 𝐺 ↑o dom 𝐹 ) ) )
66 65 simpld ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } We dom ( dom 𝐺 CNF dom 𝐹 ) )
67 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) }
68 67 f1owe ⊢ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑈 –1-1-onto→ dom ( dom 𝐺 CNF dom 𝐹 ) → ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } We dom ( dom 𝐺 CNF dom 𝐹 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } We 𝑈 ) )
69 62 66 68 sylc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } We 𝑈 )
70 weinxp ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
71 69 70 sylib ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
72 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
73 f1ofn ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → 𝐹 Fn dom 𝐹 )
74 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑥 ‘ 𝑧 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) )
75 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑦 ‘ 𝑧 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) )
76 74 75 breq12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
77 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 ) )
78 77 imbi1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
79 78 ralbidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
80 76 79 anbi12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
81 80 rexrn ⊢ ( 𝐹 Fn dom 𝐹 → ( ∃ 𝑧 ∈ ran 𝐹 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
82 72 73 81 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ ran 𝐹 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
83 f1ofo ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → 𝐹 : dom 𝐹 –onto→ 𝐴 )
84 forn ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐴 → ran 𝐹 = 𝐴 )
85 72 83 84 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ran 𝐹 = 𝐴 )
86 85 rexeqdv ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ ran 𝐹 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
87 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐺 ∈ V )
88 cnvexg ⊢ ( 𝐺 ∈ V → ◡ 𝐺 ∈ V )
89 87 88 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ◡ 𝐺 ∈ V )
90 vex ⊢ 𝑥 ∈ V
91 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐹 ∈ V )
92 coexg ⊢ ( ( 𝑥 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
93 90 91 92 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
94 coexg ⊢ ( ( ◡ 𝐺 ∈ V ∧ ( 𝑥 ∘ 𝐹 ) ∈ V ) → ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∈ V )
95 89 93 94 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∈ V )
96 vex ⊢ 𝑦 ∈ V
97 coexg ⊢ ( ( 𝑦 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
98 96 91 97 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
99 coexg ⊢ ( ( ◡ 𝐺 ∈ V ∧ ( 𝑦 ∘ 𝐹 ) ∈ V ) → ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ∈ V )
100 89 98 99 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ∈ V )
101 fveq1 ⊢ ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) → ( 𝑎 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) )
102 fveq1 ⊢ ( 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) → ( 𝑏 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) )
103 eleq12 ⊢ ( ( ( 𝑎 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ( 𝑏 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) → ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) )
104 101 102 103 syl2an ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) )
105 fveq1 ⊢ ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) → ( 𝑎 ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) )
106 fveq1 ⊢ ( 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) → ( 𝑏 ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) )
107 105 106 eqeqan12d ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) )
108 107 imbi2d ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ↔ ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
109 108 ralbidv ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
110 104 109 anbi12d ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) ↔ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
111 110 rexbidv ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
112 111 64 brabga ⊢ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∈ V ∧ ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ∈ V ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
113 95 100 112 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
114 eqid ⊢ ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) = ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) )
115 coeq1 ⊢ ( 𝑓 = 𝑥 → ( 𝑓 ∘ 𝐹 ) = ( 𝑥 ∘ 𝐹 ) )
116 115 coeq2d ⊢ ( 𝑓 = 𝑥 → ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) )
117 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
118 114 116 117 95 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) )
119 coeq1 ⊢ ( 𝑓 = 𝑦 → ( 𝑓 ∘ 𝐹 ) = ( 𝑦 ∘ 𝐹 ) )
120 119 coeq2d ⊢ ( 𝑓 = 𝑦 → ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) )
121 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
122 114 120 121 100 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) )
123 118 122 breq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ↔ ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) )
124 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) )
125 isocnv ⊢ ( 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) → ◡ 𝐺 Isom 𝑆 , E ( 𝐵 , dom 𝐺 ) )
126 124 125 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ◡ 𝐺 Isom 𝑆 , E ( 𝐵 , dom 𝐺 ) )
127 2 ssrab3 ⊢ 𝑈 ⊆ ( 𝐵 ↑m 𝐴 )
128 127 117 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) )
129 elmapi ⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑥 : 𝐴 ⟶ 𝐵 )
130 128 129 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 : 𝐴 ⟶ 𝐵 )
131 6 oif ⊢ 𝐹 : dom 𝐹 ⟶ 𝐴
132 131 ffvelcdmi ⊢ ( 𝑐 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 )
133 ffvelcdm ⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
134 130 132 133 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
135 127 121 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ ( 𝐵 ↑m 𝐴 ) )
136 elmapi ⊢ ( 𝑦 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
137 135 136 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 : 𝐴 ⟶ 𝐵 )
138 ffvelcdm ⊢ ( ( 𝑦 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 ) → ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
139 137 132 138 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
140 isorel ⊢ ( ( ◡ 𝐺 Isom 𝑆 , E ( 𝐵 , dom 𝐺 ) ∧ ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 ∧ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 ) ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) E ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
141 126 134 139 140 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) E ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
142 fvex ⊢ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ V
143 142 epeli ⊢ ( ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) E ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
144 141 143 bitrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
145 130 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝑥 : 𝐴 ⟶ 𝐵 )
146 fco ⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : dom 𝐹 ⟶ 𝐴 ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
147 145 131 146 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
148 fvco3 ⊢ ( ( ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) ) )
149 147 148 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) ) )
150 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝑐 ∈ dom 𝐹 )
151 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) )
152 131 150 151 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) )
153 152 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) ) = ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
154 149 153 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
155 137 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
156 fco ⊢ ( ( 𝑦 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : dom 𝐹 ⟶ 𝐴 ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
157 155 131 156 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
158 fvco3 ⊢ ( ( ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) ) )
159 157 158 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) ) )
160 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) )
161 131 150 160 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) )
162 161 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) ) = ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
163 159 162 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
164 154 163 eleq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
165 144 164 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) )
166 85 raleqdv ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∀ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
167 breq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
168 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ 𝑤 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
169 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( 𝑦 ‘ 𝑤 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
170 168 169 eqeq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
171 167 170 imbi12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
172 171 ralrn ⊢ ( 𝐹 Fn dom 𝐹 → ( ∀ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
173 72 73 172 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∀ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
174 166 173 bitr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
175 174 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
176 epel ⊢ ( 𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑 )
177 14 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
178 isorel ⊢ ( ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 E 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
179 177 178 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 E 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
180 176 179 bitr3id ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 ∈ 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
181 147 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
182 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝑑 ∈ dom 𝐹 )
183 181 182 fvco3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) )
184 157 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
185 184 182 fvco3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
186 183 185 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ) )
187 30 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 )
188 f1of1 ⊢ ( ◡ 𝐺 : 𝐵 –1-1-onto→ dom 𝐺 → ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 )
189 187 22 188 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 )
190 181 182 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 )
191 184 182 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 )
192 f1fveq ⊢ ( ( ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 ∧ ( ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 ∧ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 ) ) → ( ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ↔ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
193 189 190 191 192 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ↔ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
194 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
195 131 182 194 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
196 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
197 131 182 196 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
198 195 197 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
199 186 193 198 3bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
200 180 199 imbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
201 200 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
202 201 ralbidva ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
203 175 202 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
204 165 203 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
205 204 rexbidva ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
206 113 123 205 3bitr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) )
207 82 86 206 3bitr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) )
208 207 ex ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) ) )
209 208 pm5.32rd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ↔ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ) )
210 209 opabbidv ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) } )
211 df-xp ⊢ ( 𝑈 × 𝑈 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) }
212 1 211 ineq12i ⊢ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } )
213 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
214 212 213 eqtri ⊢ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
215 211 ineq2i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } )
216 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
217 215 216 eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
218 210 214 217 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) )
219 weeq1 ⊢ ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) → ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ) )
220 218 219 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ) )
221 71 220 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
222 weinxp ⊢ ( 𝑇 We 𝑈 ↔ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
223 221 222 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝑇 We 𝑈 )
224 223 ex ⊢ ( 𝜑 → ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑇 We 𝑈 ) )
225 we0 ⊢ 𝑇 We ∅
226 elmapex ⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
227 226 con3i ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ¬ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) )
228 227 pm2.21d ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → ¬ 𝑥 finSupp 𝑍 ) )
229 228 ralrimiv ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
230 rabeq0 ⊢ ( { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ ↔ ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
231 229 230 sylibr ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ )
232 2 231 eqtrid ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑈 = ∅ )
233 weeq2 ⊢ ( 𝑈 = ∅ → ( 𝑇 We 𝑈 ↔ 𝑇 We ∅ ) )
234 232 233 syl ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑇 We 𝑈 ↔ 𝑇 We ∅ ) )
235 225 234 mpbiri ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑇 We 𝑈 )
236 224 235 pm2.61d1 ⊢ ( 𝜑 → 𝑇 We 𝑈 )