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 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } We dom ( dom 𝐺 CNF dom 𝐹 ) ) )
69 68 biimprd ⊢ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑈 –1-1-onto→ dom ( dom 𝐺 CNF dom 𝐹 ) → ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } We dom ( dom 𝐺 CNF dom 𝐹 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } We 𝑈 ) )
70 62 66 69 sylc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } We 𝑈 )
71 weinxp ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
72 70 71 sylib ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
73 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
74 f1ofn ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → 𝐹 Fn dom 𝐹 )
75 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑥 ‘ 𝑧 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) )
76 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑦 ‘ 𝑧 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) )
77 75 76 breq12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
78 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 ) )
79 78 imbi1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
80 79 ralbidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
81 77 80 anbi12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
82 81 rexrn ⊢ ( 𝐹 Fn dom 𝐹 → ( ∃ 𝑧 ∈ ran 𝐹 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
83 73 74 82 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ ran 𝐹 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
84 f1ofo ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → 𝐹 : dom 𝐹 –onto→ 𝐴 )
85 forn ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐴 → ran 𝐹 = 𝐴 )
86 73 84 85 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ran 𝐹 = 𝐴 )
87 86 rexeqdv ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ ran 𝐹 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
88 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐺 ∈ V )
89 cnvexg ⊢ ( 𝐺 ∈ V → ◡ 𝐺 ∈ V )
90 88 89 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ◡ 𝐺 ∈ V )
91 vex ⊢ 𝑥 ∈ V
92 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐹 ∈ V )
93 coexg ⊢ ( ( 𝑥 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
94 91 92 93 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
95 90 94 coexd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∈ V )
96 vex ⊢ 𝑦 ∈ V
97 coexg ⊢ ( ( 𝑦 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
98 96 92 97 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
99 90 98 coexd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ∈ V )
100 fveq1 ⊢ ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) → ( 𝑎 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) )
101 fveq1 ⊢ ( 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) → ( 𝑏 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) )
102 eleq12 ⊢ ( ( ( 𝑎 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ( 𝑏 ‘ 𝑐 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) → ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) )
103 100 101 102 syl2an ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) )
104 fveq1 ⊢ ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) → ( 𝑎 ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) )
105 fveq1 ⊢ ( 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) → ( 𝑏 ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) )
106 104 105 eqeqan12d ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) )
107 106 imbi2d ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ↔ ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
108 107 ralbidv ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
109 103 108 anbi12d ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) ↔ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
110 109 rexbidv ⊢ ( ( 𝑎 = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∧ 𝑏 = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
111 110 64 brabga ⊢ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ∈ V ∧ ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ∈ V ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
112 95 99 111 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
113 eqid ⊢ ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) = ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) )
114 coeq1 ⊢ ( 𝑓 = 𝑥 → ( 𝑓 ∘ 𝐹 ) = ( 𝑥 ∘ 𝐹 ) )
115 114 coeq2d ⊢ ( 𝑓 = 𝑥 → ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) )
116 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
117 113 115 116 95 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) = ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) )
118 coeq1 ⊢ ( 𝑓 = 𝑦 → ( 𝑓 ∘ 𝐹 ) = ( 𝑦 ∘ 𝐹 ) )
119 118 coeq2d ⊢ ( 𝑓 = 𝑦 → ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) )
120 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
121 113 119 120 99 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) = ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) )
122 117 121 breq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ↔ ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ) )
123 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) )
124 isocnv ⊢ ( 𝐺 Isom E , 𝑆 ( dom 𝐺 , 𝐵 ) → ◡ 𝐺 Isom 𝑆 , E ( 𝐵 , dom 𝐺 ) )
125 123 124 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ◡ 𝐺 Isom 𝑆 , E ( 𝐵 , dom 𝐺 ) )
126 2 ssrab3 ⊢ 𝑈 ⊆ ( 𝐵 ↑m 𝐴 )
127 126 116 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) )
128 elmapi ⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑥 : 𝐴 ⟶ 𝐵 )
129 127 128 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 : 𝐴 ⟶ 𝐵 )
130 6 oif ⊢ 𝐹 : dom 𝐹 ⟶ 𝐴
131 130 ffvelcdmi ⊢ ( 𝑐 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 )
132 ffvelcdm ⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
133 129 131 132 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
134 126 120 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ ( 𝐵 ↑m 𝐴 ) )
135 elmapi ⊢ ( 𝑦 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
136 134 135 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 : 𝐴 ⟶ 𝐵 )
137 ffvelcdm ⊢ ( ( 𝑦 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐴 ) → ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
138 136 131 137 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 )
139 isorel ⊢ ( ( ◡ 𝐺 Isom 𝑆 , E ( 𝐵 , dom 𝐺 ) ∧ ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 ∧ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐵 ) ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) E ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
140 125 133 138 139 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) E ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
141 fvex ⊢ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ V
142 141 epeli ⊢ ( ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) E ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
143 140 142 bitrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
144 129 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝑥 : 𝐴 ⟶ 𝐵 )
145 fco ⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : dom 𝐹 ⟶ 𝐴 ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
146 144 130 145 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
147 fvco3 ⊢ ( ( ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) ) )
148 146 147 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) ) )
149 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝑐 ∈ dom 𝐹 )
150 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) )
151 130 149 150 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) )
152 151 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑐 ) ) = ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
153 148 152 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
154 136 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
155 fco ⊢ ( ( 𝑦 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : dom 𝐹 ⟶ 𝐴 ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
156 154 130 155 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
157 fvco3 ⊢ ( ( ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) ) )
158 156 157 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) ) )
159 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) )
160 130 149 159 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) )
161 160 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑐 ) ) = ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
162 158 161 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) = ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) )
163 153 162 eleq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ↔ ( ◡ 𝐺 ‘ ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ◡ 𝐺 ‘ ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ) ) )
164 143 163 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ) )
165 86 raleqdv ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∀ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
166 breq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
167 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ 𝑤 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
168 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( 𝑦 ‘ 𝑤 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
169 167 168 eqeq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
170 166 169 imbi12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑑 ) → ( ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
171 170 ralrn ⊢ ( 𝐹 Fn dom 𝐹 → ( ∀ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
172 73 74 171 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∀ 𝑤 ∈ ran 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
173 165 172 bitr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
174 173 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
175 epel ⊢ ( 𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑 )
176 14 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
177 isorel ⊢ ( ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 E 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
178 176 177 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 E 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
179 175 178 bitr3id ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑐 ∈ 𝑑 ↔ ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) ) )
180 146 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑥 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
181 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝑑 ∈ dom 𝐹 )
182 180 181 fvco3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) )
183 156 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( 𝑦 ∘ 𝐹 ) : dom 𝐹 ⟶ 𝐵 )
184 183 181 fvco3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
185 182 184 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ) )
186 30 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → 𝐺 : dom 𝐺 –1-1-onto→ 𝐵 )
187 f1of1 ⊢ ( ◡ 𝐺 : 𝐵 –1-1-onto→ dom 𝐺 → ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 )
188 186 22 187 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 )
189 180 181 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 )
190 183 181 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 )
191 f1fveq ⊢ ( ( ◡ 𝐺 : 𝐵 –1-1→ dom 𝐺 ∧ ( ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 ∧ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ∈ 𝐵 ) ) → ( ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ↔ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
192 188 189 190 191 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐺 ‘ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) ) = ( ◡ 𝐺 ‘ ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) ↔ ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ) )
193 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
194 130 181 193 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) )
195 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
196 130 181 195 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) )
197 194 196 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( 𝑥 ∘ 𝐹 ) ‘ 𝑑 ) = ( ( 𝑦 ∘ 𝐹 ) ‘ 𝑑 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
198 185 192 197 3bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) )
199 179 198 imbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹 ) ) → ( ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
200 199 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) ∧ 𝑑 ∈ dom 𝐹 ) → ( ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
201 200 ralbidva ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑐 ) 𝑅 ( 𝐹 ‘ 𝑑 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑑 ) ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑑 ) ) ) ) )
202 174 201 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) )
203 164 202 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ 𝑐 ∈ dom 𝐹 ) → ( ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
204 203 rexbidva ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑐 ∈ dom 𝐹 ( ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑐 ) ∈ ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( ( ◡ 𝐺 ∘ ( 𝑥 ∘ 𝐹 ) ) ‘ 𝑑 ) = ( ( ◡ 𝐺 ∘ ( 𝑦 ∘ 𝐹 ) ) ‘ 𝑑 ) ) ) ) )
205 112 122 204 3bitr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑐 ) ) 𝑆 ( 𝑦 ‘ ( 𝐹 ‘ 𝑐 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑐 ) 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) )
206 83 87 205 3bitr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) )
207 206 ex ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ) ) )
208 207 pm5.32rd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ↔ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ) )
209 208 opabbidv ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) } )
210 df-xp ⊢ ( 𝑈 × 𝑈 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) }
211 1 210 ineq12i ⊢ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } )
212 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
213 211 212 eqtri ⊢ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
214 210 ineq2i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } )
215 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
216 214 215 eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) }
217 209 213 216 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) )
218 weeq1 ⊢ ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) → ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ) )
219 217 218 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑥 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ dom 𝐹 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑑 ∈ dom 𝐹 ( 𝑐 ∈ 𝑑 → ( 𝑎 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) ) ) } ( ( 𝑓 ∈ 𝑈 ↦ ( ◡ 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ‘ 𝑦 ) } ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 ) )
220 72 219 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
221 weinxp ⊢ ( 𝑇 We 𝑈 ↔ ( 𝑇 ∩ ( 𝑈 × 𝑈 ) ) We 𝑈 )
222 220 221 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) ) → 𝑇 We 𝑈 )
223 222 ex ⊢ ( 𝜑 → ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑇 We 𝑈 ) )
224 we0 ⊢ 𝑇 We ∅
225 elmapex ⊢ ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
226 225 con3i ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ¬ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) )
227 226 pm2.21d ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) → ¬ 𝑥 finSupp 𝑍 ) )
228 227 ralrimiv ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
229 rabeq0 ⊢ ( { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ ↔ ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
230 228 229 sylibr ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ )
231 2 230 eqtrid ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑈 = ∅ )
232 weeq2 ⊢ ( 𝑈 = ∅ → ( 𝑇 We 𝑈 ↔ 𝑇 We ∅ ) )
233 231 232 syl ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑇 We 𝑈 ↔ 𝑇 We ∅ ) )
234 224 233 mpbiri ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → 𝑇 We 𝑈 )
235 223 234 pm2.61d1 ⊢ ( 𝜑 → 𝑇 We 𝑈 )