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 ffvelrni ⊢ ( ∅ ∈ 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 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ 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 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) )
129 elmapi ⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑥 : 𝐴 ⟶ 𝐵 )
130 128 129 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 : 𝐴 ⟶ 𝐵 )
131 6 oif ⊢ 𝐹 : dom 𝐹 ⟶ 𝐴
132 131 ffvelrni ⊢ ( 𝑐 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 )
133 ffvelrn ⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
134 130 132 133 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
135 127 121 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ ( 𝐵 ↑m 𝐴 ) )
136 elmapi ⊢ ( 𝑦 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
137 135 136 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 : 𝐴 ⟶ 𝐵 )
138 ffvelrn ⊢ ( ( 𝑦 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 ) → ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
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 syl6bb ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ 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 syl5bbr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 ∈ 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
181 147 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
182 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝑑 ∈ dom 𝐹 )
183 fvco3 ⊢ ( ( ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) )
184 181 182 183 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) )
185 157 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
186 fvco3 ⊢ ( ( ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
187 185 182 186 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
188 184 187 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ) )
189 30 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 )
190 f1of1 ⊢ ( ◡ 𝐺 : 𝐵 –1-1-onto→ dom 𝐺 → ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 )
191 189 22 190 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 )
192 181 182 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 )
193 185 182 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 )
194 f1fveq ⊢ ( ( ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 ∧ ( ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 ∧ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 ) ) → ( ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ↔ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
195 191 192 193 194 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ↔ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
196 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
197 131 182 196 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
198 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
199 131 182 198 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
200 197 199 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
201 188 195 200 3bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
202 180 201 imbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
203 202 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
204 203 ralbidva ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
205 175 204 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
206 165 205 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
207 206 rexbidva ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
208 113 123 207 3bitr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) )
209 82 86 208 3bitr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) )
210 209 ex ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) ) )
211 210 pm5.32rd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ↔ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ) )
212 211 opabbidv ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) } )
213 df-xp ⊢ ( 𝑈 × 𝑈 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) }
214 1 213 ineq12i ⊢ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } )
215 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
216 214 215 eqtri ⊢ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
217 213 ineq2i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } )
218 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
219 217 218 eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
220 212 216 219 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) )
221 weeq1 ⊢ ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) → ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ) )
222 220 221 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ) )
223 71 222 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
224 weinxp ⊢ ( 𝑇 We 𝑈 ↔ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
225 223 224 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝑇 We 𝑈 )
226 225 ex ⊢ ( 𝜑 → ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑇 We 𝑈 ) )
227 we0 ⊢ 𝑇 We ∅
228 elmapex ⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
229 228 con3i ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ¬ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) )
230 229 pm2.21d ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → ¬ 𝑥 finSupp 𝑍 ) )
231 230 ralrimiv ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
232 rabeq0 ⊢ ( { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ ↔ ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
233 231 232 sylibr ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ )
234 2 233 syl5eq ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑈 = ∅ )
235 weeq2 ⊢ ( 𝑈 = ∅ → ( 𝑇 We 𝑈 ↔ 𝑇 We ∅ ) )
236 234 235 syl ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑇 We 𝑈 ↔ 𝑇 We ∅ ) )
237 227 236 mpbiri ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑇 We 𝑈 )
238 226 237 pm2.61d1 ⊢ ( 𝜑 → 𝑇 We 𝑈 )