MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wemapwe Structured version   Visualization version   GIF version

Theorem wemapwe 9640
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.)
Hypotheses
Ref Expression
wemapwe.t 𝑇 = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))}
wemapwe.u π‘ˆ = {π‘₯ ∈ (𝐡 ↑m 𝐴) ∣ π‘₯ finSupp 𝑍}
wemapwe.2 (πœ‘ β†’ 𝑅 We 𝐴)
wemapwe.3 (πœ‘ β†’ 𝑆 We 𝐡)
wemapwe.4 (πœ‘ β†’ 𝐡 β‰  βˆ…)
wemapwe.5 𝐹 = OrdIso(𝑅, 𝐴)
wemapwe.6 𝐺 = OrdIso(𝑆, 𝐡)
wemapwe.7 𝑍 = (πΊβ€˜βˆ…)
Assertion
Ref Expression
wemapwe (πœ‘ β†’ 𝑇 We π‘ˆ)
Distinct variable groups:   π‘₯,𝑀,𝑦,𝑧,𝐴   π‘₯,𝐡,𝑦   𝑀,𝐹,π‘₯,𝑦,𝑧   π‘₯,𝐺,𝑦   πœ‘,π‘₯,𝑦   𝑀,𝑅,𝑧   𝑧,𝑆   π‘₯,π‘ˆ,𝑦   π‘₯,𝑍
Allowed substitution hints:   πœ‘(𝑧,𝑀)   𝐡(𝑧,𝑀)   𝑅(π‘₯,𝑦)   𝑆(π‘₯,𝑦,𝑀)   𝑇(π‘₯,𝑦,𝑧,𝑀)   π‘ˆ(𝑧,𝑀)   𝐺(𝑧,𝑀)   𝑍(𝑦,𝑧,𝑀)

Proof of Theorem wemapwe
Dummy variables π‘Ž 𝑏 𝑐 𝑑 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wemapwe.u . . . . . . . . 9 π‘ˆ = {π‘₯ ∈ (𝐡 ↑m 𝐴) ∣ π‘₯ finSupp 𝑍}
2 eqid 2737 . . . . . . . . 9 {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp (β—‘πΊβ€˜π‘)} = {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp (β—‘πΊβ€˜π‘)}
3 eqid 2737 . . . . . . . . 9 (β—‘πΊβ€˜π‘) = (β—‘πΊβ€˜π‘)
4 simprr 772 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐴 ∈ V)
5 wemapwe.2 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 We 𝐴)
65adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝑅 We 𝐴)
7 wemapwe.5 . . . . . . . . . . . 12 𝐹 = OrdIso(𝑅, 𝐴)
87oiiso 9480 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ 𝑅 We 𝐴) β†’ 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
94, 6, 8syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
10 isof1o 7273 . . . . . . . . . 10 (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) β†’ 𝐹:dom 𝐹–1-1-onto→𝐴)
119, 10syl 17 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐹:dom 𝐹–1-1-onto→𝐴)
12 simprl 770 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐡 ∈ V)
13 wemapwe.3 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 We 𝐡)
1413adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝑆 We 𝐡)
15 wemapwe.6 . . . . . . . . . . . 12 𝐺 = OrdIso(𝑆, 𝐡)
1615oiiso 9480 . . . . . . . . . . 11 ((𝐡 ∈ V ∧ 𝑆 We 𝐡) β†’ 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐡))
1712, 14, 16syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐡))
18 isof1o 7273 . . . . . . . . . 10 (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐡) β†’ 𝐺:dom 𝐺–1-1-onto→𝐡)
19 f1ocnv 6801 . . . . . . . . . 10 (𝐺:dom 𝐺–1-1-onto→𝐡 β†’ ◑𝐺:𝐡–1-1-ontoβ†’dom 𝐺)
2017, 18, 193syl 18 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ◑𝐺:𝐡–1-1-ontoβ†’dom 𝐺)
217oiexg 9478 . . . . . . . . . . 11 (𝐴 ∈ V β†’ 𝐹 ∈ V)
2221ad2antll 728 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐹 ∈ V)
2322dmexd 7847 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom 𝐹 ∈ V)
2415oiexg 9478 . . . . . . . . . . 11 (𝐡 ∈ V β†’ 𝐺 ∈ V)
2524ad2antrl 727 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐺 ∈ V)
2625dmexd 7847 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom 𝐺 ∈ V)
27 wemapwe.7 . . . . . . . . . 10 𝑍 = (πΊβ€˜βˆ…)
2817, 18syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐺:dom 𝐺–1-1-onto→𝐡)
29 f1ofo 6796 . . . . . . . . . . . . . . 15 (𝐺:dom 𝐺–1-1-onto→𝐡 β†’ 𝐺:dom 𝐺–onto→𝐡)
30 forn 6764 . . . . . . . . . . . . . . 15 (𝐺:dom 𝐺–onto→𝐡 β†’ ran 𝐺 = 𝐡)
3128, 29, 303syl 18 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ran 𝐺 = 𝐡)
32 wemapwe.4 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐡 β‰  βˆ…)
3332adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝐡 β‰  βˆ…)
3431, 33eqnetrd 3012 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ran 𝐺 β‰  βˆ…)
35 dm0rn0 5885 . . . . . . . . . . . . . 14 (dom 𝐺 = βˆ… ↔ ran 𝐺 = βˆ…)
3635necon3bii 2997 . . . . . . . . . . . . 13 (dom 𝐺 β‰  βˆ… ↔ ran 𝐺 β‰  βˆ…)
3734, 36sylibr 233 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom 𝐺 β‰  βˆ…)
3815oicl 9472 . . . . . . . . . . . . 13 Ord dom 𝐺
39 ord0eln0 6377 . . . . . . . . . . . . 13 (Ord dom 𝐺 β†’ (βˆ… ∈ dom 𝐺 ↔ dom 𝐺 β‰  βˆ…))
4038, 39ax-mp 5 . . . . . . . . . . . 12 (βˆ… ∈ dom 𝐺 ↔ dom 𝐺 β‰  βˆ…)
4137, 40sylibr 233 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ βˆ… ∈ dom 𝐺)
4215oif 9473 . . . . . . . . . . . 12 𝐺:dom 𝐺⟢𝐡
4342ffvelcdmi 7039 . . . . . . . . . . 11 (βˆ… ∈ dom 𝐺 β†’ (πΊβ€˜βˆ…) ∈ 𝐡)
4441, 43syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (πΊβ€˜βˆ…) ∈ 𝐡)
4527, 44eqeltrid 2842 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝑍 ∈ 𝐡)
461, 2, 3, 11, 20, 4, 12, 23, 26, 45mapfien 9351 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹))):π‘ˆβ€“1-1-ontoβ†’{π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp (β—‘πΊβ€˜π‘)})
47 eqid 2737 . . . . . . . . . . 11 {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp βˆ…} = {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp βˆ…}
4815oion 9479 . . . . . . . . . . . 12 (𝐡 ∈ V β†’ dom 𝐺 ∈ On)
4948ad2antrl 727 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom 𝐺 ∈ On)
507oion 9479 . . . . . . . . . . . 12 (𝐴 ∈ V β†’ dom 𝐹 ∈ On)
5150ad2antll 728 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom 𝐹 ∈ On)
5247, 49, 51cantnfdm 9607 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom (dom 𝐺 CNF dom 𝐹) = {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp βˆ…})
5327fveq2i 6850 . . . . . . . . . . . . 13 (β—‘πΊβ€˜π‘) = (β—‘πΊβ€˜(πΊβ€˜βˆ…))
54 f1ocnvfv1 7227 . . . . . . . . . . . . . 14 ((𝐺:dom 𝐺–1-1-onto→𝐡 ∧ βˆ… ∈ dom 𝐺) β†’ (β—‘πΊβ€˜(πΊβ€˜βˆ…)) = βˆ…)
5528, 41, 54syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (β—‘πΊβ€˜(πΊβ€˜βˆ…)) = βˆ…)
5653, 55eqtrid 2789 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (β—‘πΊβ€˜π‘) = βˆ…)
5756breq2d 5122 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (π‘₯ finSupp (β—‘πΊβ€˜π‘) ↔ π‘₯ finSupp βˆ…))
5857rabbidv 3418 . . . . . . . . . 10 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp (β—‘πΊβ€˜π‘)} = {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp βˆ…})
5952, 58eqtr4d 2780 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ dom (dom 𝐺 CNF dom 𝐹) = {π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp (β—‘πΊβ€˜π‘)})
6059f1oeq3d 6786 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹))):π‘ˆβ€“1-1-ontoβ†’dom (dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹))):π‘ˆβ€“1-1-ontoβ†’{π‘₯ ∈ (dom 𝐺 ↑m dom 𝐹) ∣ π‘₯ finSupp (β—‘πΊβ€˜π‘)}))
6146, 60mpbird 257 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹))):π‘ˆβ€“1-1-ontoβ†’dom (dom 𝐺 CNF dom 𝐹))
62 eqid 2737 . . . . . . . . 9 dom (dom 𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹)
63 eqid 2737 . . . . . . . . 9 {βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} = {βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))}
6462, 49, 51, 63oemapwe 9637 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ({βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑o dom 𝐹)))
6564simpld 496 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} We dom (dom 𝐺 CNF dom 𝐹))
66 eqid 2737 . . . . . . . 8 {⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} = {⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)}
6766f1owe 7303 . . . . . . 7 ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹))):π‘ˆβ€“1-1-ontoβ†’dom (dom 𝐺 CNF dom 𝐹) β†’ ({βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} We dom (dom 𝐺 CNF dom 𝐹) β†’ {⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} We π‘ˆ))
6861, 65, 67sylc 65 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} We π‘ˆ)
69 weinxp 5721 . . . . . 6 ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} We π‘ˆ ↔ ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ)
7068, 69sylib 217 . . . . 5 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ)
7111adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ 𝐹:dom 𝐹–1-1-onto→𝐴)
72 f1ofn 6790 . . . . . . . . . . . 12 (𝐹:dom 𝐹–1-1-onto→𝐴 β†’ 𝐹 Fn dom 𝐹)
73 fveq2 6847 . . . . . . . . . . . . . . 15 (𝑧 = (πΉβ€˜π‘) β†’ (π‘₯β€˜π‘§) = (π‘₯β€˜(πΉβ€˜π‘)))
74 fveq2 6847 . . . . . . . . . . . . . . 15 (𝑧 = (πΉβ€˜π‘) β†’ (π‘¦β€˜π‘§) = (π‘¦β€˜(πΉβ€˜π‘)))
7573, 74breq12d 5123 . . . . . . . . . . . . . 14 (𝑧 = (πΉβ€˜π‘) β†’ ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ↔ (π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘))))
76 breq1 5113 . . . . . . . . . . . . . . . 16 (𝑧 = (πΉβ€˜π‘) β†’ (𝑧𝑅𝑀 ↔ (πΉβ€˜π‘)𝑅𝑀))
7776imbi1d 342 . . . . . . . . . . . . . . 15 (𝑧 = (πΉβ€˜π‘) β†’ ((𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))))
7877ralbidv 3175 . . . . . . . . . . . . . 14 (𝑧 = (πΉβ€˜π‘) β†’ (βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))))
7975, 78anbi12d 632 . . . . . . . . . . . . 13 (𝑧 = (πΉβ€˜π‘) β†’ (((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ ((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ∧ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))))
8079rexrn 7042 . . . . . . . . . . . 12 (𝐹 Fn dom 𝐹 β†’ (βˆƒπ‘§ ∈ ran 𝐹((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ βˆƒπ‘ ∈ dom 𝐹((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ∧ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))))
8171, 72, 803syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆƒπ‘§ ∈ ran 𝐹((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ βˆƒπ‘ ∈ dom 𝐹((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ∧ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))))
82 f1ofo 6796 . . . . . . . . . . . . 13 (𝐹:dom 𝐹–1-1-onto→𝐴 β†’ 𝐹:dom 𝐹–onto→𝐴)
83 forn 6764 . . . . . . . . . . . . 13 (𝐹:dom 𝐹–onto→𝐴 β†’ ran 𝐹 = 𝐴)
8471, 82, 833syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ ran 𝐹 = 𝐴)
8584rexeqdv 3317 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆƒπ‘§ ∈ ran 𝐹((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))))
8625adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ 𝐺 ∈ V)
87 cnvexg 7866 . . . . . . . . . . . . . . 15 (𝐺 ∈ V β†’ ◑𝐺 ∈ V)
8886, 87syl 17 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ ◑𝐺 ∈ V)
89 vex 3452 . . . . . . . . . . . . . . 15 π‘₯ ∈ V
9022adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ 𝐹 ∈ V)
91 coexg 7871 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ V ∧ 𝐹 ∈ V) β†’ (π‘₯ ∘ 𝐹) ∈ V)
9289, 90, 91sylancr 588 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (π‘₯ ∘ 𝐹) ∈ V)
93 coexg 7871 . . . . . . . . . . . . . 14 ((◑𝐺 ∈ V ∧ (π‘₯ ∘ 𝐹) ∈ V) β†’ (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∈ V)
9488, 92, 93syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∈ V)
95 vex 3452 . . . . . . . . . . . . . . 15 𝑦 ∈ V
96 coexg 7871 . . . . . . . . . . . . . . 15 ((𝑦 ∈ V ∧ 𝐹 ∈ V) β†’ (𝑦 ∘ 𝐹) ∈ V)
9795, 90, 96sylancr 588 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (𝑦 ∘ 𝐹) ∈ V)
98 coexg 7871 . . . . . . . . . . . . . 14 ((◑𝐺 ∈ V ∧ (𝑦 ∘ 𝐹) ∈ V) β†’ (◑𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
9988, 97, 98syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (◑𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
100 fveq1 6846 . . . . . . . . . . . . . . . . 17 (π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) β†’ (π‘Žβ€˜π‘) = ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘))
101 fveq1 6846 . . . . . . . . . . . . . . . . 17 (𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹)) β†’ (π‘β€˜π‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘))
102 eleq12 2828 . . . . . . . . . . . . . . . . 17 (((π‘Žβ€˜π‘) = ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∧ (π‘β€˜π‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘)) β†’ ((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ↔ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘)))
103100, 101, 102syl2an 597 . . . . . . . . . . . . . . . 16 ((π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∧ 𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹))) β†’ ((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ↔ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘)))
104 fveq1 6846 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) β†’ (π‘Žβ€˜π‘‘) = ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘))
105 fveq1 6846 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹)) β†’ (π‘β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘))
106104, 105eqeqan12d 2751 . . . . . . . . . . . . . . . . . 18 ((π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∧ 𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹))) β†’ ((π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘) ↔ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))
107106imbi2d 341 . . . . . . . . . . . . . . . . 17 ((π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∧ 𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹))) β†’ ((𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)) ↔ (𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘))))
108107ralbidv 3175 . . . . . . . . . . . . . . . 16 ((π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∧ 𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹))) β†’ (βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)) ↔ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘))))
109103, 108anbi12d 632 . . . . . . . . . . . . . . 15 ((π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∧ 𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹))) β†’ (((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘))) ↔ (((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))))
110109rexbidv 3176 . . . . . . . . . . . . . 14 ((π‘Ž = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∧ 𝑏 = (◑𝐺 ∘ (𝑦 ∘ 𝐹))) β†’ (βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘))) ↔ βˆƒπ‘ ∈ dom 𝐹(((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))))
111110, 63brabga 5496 . . . . . . . . . . . . 13 (((◑𝐺 ∘ (π‘₯ ∘ 𝐹)) ∈ V ∧ (◑𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹)){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} (◑𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ βˆƒπ‘ ∈ dom 𝐹(((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))))
11294, 99, 111syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹)){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} (◑𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ βˆƒπ‘ ∈ dom 𝐹(((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))))
113 eqid 2737 . . . . . . . . . . . . . 14 (𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))
114 coeq1 5818 . . . . . . . . . . . . . . 15 (𝑓 = π‘₯ β†’ (𝑓 ∘ 𝐹) = (π‘₯ ∘ 𝐹))
115114coeq2d 5823 . . . . . . . . . . . . . 14 (𝑓 = π‘₯ β†’ (◑𝐺 ∘ (𝑓 ∘ 𝐹)) = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)))
116 simprl 770 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ π‘₯ ∈ π‘ˆ)
117113, 115, 116, 94fvmptd3 6976 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯) = (◑𝐺 ∘ (π‘₯ ∘ 𝐹)))
118 coeq1 5818 . . . . . . . . . . . . . . 15 (𝑓 = 𝑦 β†’ (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹))
119118coeq2d 5823 . . . . . . . . . . . . . 14 (𝑓 = 𝑦 β†’ (◑𝐺 ∘ (𝑓 ∘ 𝐹)) = (◑𝐺 ∘ (𝑦 ∘ 𝐹)))
120 simprr 772 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ 𝑦 ∈ π‘ˆ)
121113, 119, 120, 99fvmptd3 6976 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦) = (◑𝐺 ∘ (𝑦 ∘ 𝐹)))
122117, 121breq12d 5123 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦) ↔ (◑𝐺 ∘ (π‘₯ ∘ 𝐹)){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} (◑𝐺 ∘ (𝑦 ∘ 𝐹))))
12317ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐡))
124 isocnv 7280 . . . . . . . . . . . . . . . . . 18 (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐡) β†’ ◑𝐺 Isom 𝑆, E (𝐡, dom 𝐺))
125123, 124syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ◑𝐺 Isom 𝑆, E (𝐡, dom 𝐺))
1261ssrab3 4045 . . . . . . . . . . . . . . . . . . . 20 π‘ˆ βŠ† (𝐡 ↑m 𝐴)
127126, 116sselid 3947 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ π‘₯ ∈ (𝐡 ↑m 𝐴))
128 elmapi 8794 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (𝐡 ↑m 𝐴) β†’ π‘₯:𝐴⟢𝐡)
129127, 128syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ π‘₯:𝐴⟢𝐡)
1307oif 9473 . . . . . . . . . . . . . . . . . . 19 𝐹:dom 𝐹⟢𝐴
131130ffvelcdmi 7039 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ dom 𝐹 β†’ (πΉβ€˜π‘) ∈ 𝐴)
132 ffvelcdm 7037 . . . . . . . . . . . . . . . . . 18 ((π‘₯:𝐴⟢𝐡 ∧ (πΉβ€˜π‘) ∈ 𝐴) β†’ (π‘₯β€˜(πΉβ€˜π‘)) ∈ 𝐡)
133129, 131, 132syl2an 597 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (π‘₯β€˜(πΉβ€˜π‘)) ∈ 𝐡)
134126, 120sselid 3947 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ 𝑦 ∈ (𝐡 ↑m 𝐴))
135 elmapi 8794 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐡 ↑m 𝐴) β†’ 𝑦:𝐴⟢𝐡)
136134, 135syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ 𝑦:𝐴⟢𝐡)
137 ffvelcdm 7037 . . . . . . . . . . . . . . . . . 18 ((𝑦:𝐴⟢𝐡 ∧ (πΉβ€˜π‘) ∈ 𝐴) β†’ (π‘¦β€˜(πΉβ€˜π‘)) ∈ 𝐡)
138136, 131, 137syl2an 597 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (π‘¦β€˜(πΉβ€˜π‘)) ∈ 𝐡)
139 isorel 7276 . . . . . . . . . . . . . . . . 17 ((◑𝐺 Isom 𝑆, E (𝐡, dom 𝐺) ∧ ((π‘₯β€˜(πΉβ€˜π‘)) ∈ 𝐡 ∧ (π‘¦β€˜(πΉβ€˜π‘)) ∈ 𝐡)) β†’ ((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ↔ (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))) E (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘)))))
140125, 133, 138, 139syl12anc 836 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ↔ (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))) E (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘)))))
141 fvex 6860 . . . . . . . . . . . . . . . . 17 (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘))) ∈ V
142141epeli 5544 . . . . . . . . . . . . . . . 16 ((β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))) E (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘))) ↔ (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))) ∈ (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘))))
143140, 142bitrdi 287 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ↔ (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))) ∈ (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘)))))
144129adantr 482 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ π‘₯:𝐴⟢𝐡)
145 fco 6697 . . . . . . . . . . . . . . . . . . 19 ((π‘₯:𝐴⟢𝐡 ∧ 𝐹:dom 𝐹⟢𝐴) β†’ (π‘₯ ∘ 𝐹):dom 𝐹⟢𝐡)
146144, 130, 145sylancl 587 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (π‘₯ ∘ 𝐹):dom 𝐹⟢𝐡)
147 fvco3 6945 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∘ 𝐹):dom 𝐹⟢𝐡 ∧ 𝑐 ∈ dom 𝐹) β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) = (β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘)))
148146, 147sylancom 589 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) = (β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘)))
149 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ 𝑐 ∈ dom 𝐹)
150 fvco3 6945 . . . . . . . . . . . . . . . . . . 19 ((𝐹:dom 𝐹⟢𝐴 ∧ 𝑐 ∈ dom 𝐹) β†’ ((π‘₯ ∘ 𝐹)β€˜π‘) = (π‘₯β€˜(πΉβ€˜π‘)))
151130, 149, 150sylancr 588 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((π‘₯ ∘ 𝐹)β€˜π‘) = (π‘₯β€˜(πΉβ€˜π‘)))
152151fveq2d 6851 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘)) = (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))))
153148, 152eqtrd 2777 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) = (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))))
154136adantr 482 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ 𝑦:𝐴⟢𝐡)
155 fco 6697 . . . . . . . . . . . . . . . . . . 19 ((𝑦:𝐴⟢𝐡 ∧ 𝐹:dom 𝐹⟢𝐴) β†’ (𝑦 ∘ 𝐹):dom 𝐹⟢𝐡)
156154, 130, 155sylancl 587 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (𝑦 ∘ 𝐹):dom 𝐹⟢𝐡)
157 fvco3 6945 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∘ 𝐹):dom 𝐹⟢𝐡 ∧ 𝑐 ∈ dom 𝐹) β†’ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) = (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘)))
158156, 157sylancom 589 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) = (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘)))
159 fvco3 6945 . . . . . . . . . . . . . . . . . . 19 ((𝐹:dom 𝐹⟢𝐴 ∧ 𝑐 ∈ dom 𝐹) β†’ ((𝑦 ∘ 𝐹)β€˜π‘) = (π‘¦β€˜(πΉβ€˜π‘)))
160130, 149, 159sylancr 588 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((𝑦 ∘ 𝐹)β€˜π‘) = (π‘¦β€˜(πΉβ€˜π‘)))
161160fveq2d 6851 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘)) = (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘))))
162158, 161eqtrd 2777 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) = (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘))))
163153, 162eleq12d 2832 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ↔ (β—‘πΊβ€˜(π‘₯β€˜(πΉβ€˜π‘))) ∈ (β—‘πΊβ€˜(π‘¦β€˜(πΉβ€˜π‘)))))
164143, 163bitr4d 282 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ ((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ↔ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘)))
16584raleqdv 3316 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆ€π‘€ ∈ ran 𝐹((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))))
166 breq2 5114 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = (πΉβ€˜π‘‘) β†’ ((πΉβ€˜π‘)𝑅𝑀 ↔ (πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘)))
167 fveq2 6847 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = (πΉβ€˜π‘‘) β†’ (π‘₯β€˜π‘€) = (π‘₯β€˜(πΉβ€˜π‘‘)))
168 fveq2 6847 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = (πΉβ€˜π‘‘) β†’ (π‘¦β€˜π‘€) = (π‘¦β€˜(πΉβ€˜π‘‘)))
169167, 168eqeq12d 2753 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = (πΉβ€˜π‘‘) β†’ ((π‘₯β€˜π‘€) = (π‘¦β€˜π‘€) ↔ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘))))
170166, 169imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (𝑀 = (πΉβ€˜π‘‘) β†’ (((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ ((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
171170ralrn 7043 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn dom 𝐹 β†’ (βˆ€π‘€ ∈ ran 𝐹((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘‘ ∈ dom 𝐹((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
17271, 72, 1713syl 18 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆ€π‘€ ∈ ran 𝐹((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘‘ ∈ dom 𝐹((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
173165, 172bitr3d 281 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘‘ ∈ dom 𝐹((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
174173adantr 482 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘‘ ∈ dom 𝐹((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
175 epel 5545 . . . . . . . . . . . . . . . . . . 19 (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑)
1769ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
177 isorel 7276 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (𝑐 E 𝑑 ↔ (πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘)))
178176, 177sylancom 589 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (𝑐 E 𝑑 ↔ (πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘)))
179175, 178bitr3id 285 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (𝑐 ∈ 𝑑 ↔ (πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘)))
180146adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (π‘₯ ∘ 𝐹):dom 𝐹⟢𝐡)
181 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ 𝑑 ∈ dom 𝐹)
182180, 181fvco3d 6946 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = (β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘‘)))
183156adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (𝑦 ∘ 𝐹):dom 𝐹⟢𝐡)
184183, 181fvco3d 6946 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘) = (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘‘)))
185182, 184eqeq12d 2753 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘) ↔ (β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘‘)) = (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘‘))))
18628ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ 𝐺:dom 𝐺–1-1-onto→𝐡)
187 f1of1 6788 . . . . . . . . . . . . . . . . . . . . 21 (◑𝐺:𝐡–1-1-ontoβ†’dom 𝐺 β†’ ◑𝐺:𝐡–1-1β†’dom 𝐺)
188186, 19, 1873syl 18 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ◑𝐺:𝐡–1-1β†’dom 𝐺)
189180, 181ffvelcdmd 7041 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((π‘₯ ∘ 𝐹)β€˜π‘‘) ∈ 𝐡)
190183, 181ffvelcdmd 7041 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((𝑦 ∘ 𝐹)β€˜π‘‘) ∈ 𝐡)
191 f1fveq 7214 . . . . . . . . . . . . . . . . . . . 20 ((◑𝐺:𝐡–1-1β†’dom 𝐺 ∧ (((π‘₯ ∘ 𝐹)β€˜π‘‘) ∈ 𝐡 ∧ ((𝑦 ∘ 𝐹)β€˜π‘‘) ∈ 𝐡)) β†’ ((β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘‘)) = (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘‘)) ↔ ((π‘₯ ∘ 𝐹)β€˜π‘‘) = ((𝑦 ∘ 𝐹)β€˜π‘‘)))
192188, 189, 190, 191syl12anc 836 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((β—‘πΊβ€˜((π‘₯ ∘ 𝐹)β€˜π‘‘)) = (β—‘πΊβ€˜((𝑦 ∘ 𝐹)β€˜π‘‘)) ↔ ((π‘₯ ∘ 𝐹)β€˜π‘‘) = ((𝑦 ∘ 𝐹)β€˜π‘‘)))
193 fvco3 6945 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:dom 𝐹⟢𝐴 ∧ 𝑑 ∈ dom 𝐹) β†’ ((π‘₯ ∘ 𝐹)β€˜π‘‘) = (π‘₯β€˜(πΉβ€˜π‘‘)))
194130, 181, 193sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((π‘₯ ∘ 𝐹)β€˜π‘‘) = (π‘₯β€˜(πΉβ€˜π‘‘)))
195 fvco3 6945 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:dom 𝐹⟢𝐴 ∧ 𝑑 ∈ dom 𝐹) β†’ ((𝑦 ∘ 𝐹)β€˜π‘‘) = (π‘¦β€˜(πΉβ€˜π‘‘)))
196130, 181, 195sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((𝑦 ∘ 𝐹)β€˜π‘‘) = (π‘¦β€˜(πΉβ€˜π‘‘)))
197194, 196eqeq12d 2753 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (((π‘₯ ∘ 𝐹)β€˜π‘‘) = ((𝑦 ∘ 𝐹)β€˜π‘‘) ↔ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘))))
198185, 192, 1973bitrd 305 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ (((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘) ↔ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘))))
199179, 198imbi12d 345 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) β†’ ((𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)) ↔ ((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
200199anassrs 469 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) β†’ ((𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)) ↔ ((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
201200ralbidva 3173 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)) ↔ βˆ€π‘‘ ∈ dom 𝐹((πΉβ€˜π‘)𝑅(πΉβ€˜π‘‘) β†’ (π‘₯β€˜(πΉβ€˜π‘‘)) = (π‘¦β€˜(πΉβ€˜π‘‘)))))
202174, 201bitr4d 282 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)) ↔ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘))))
203164, 202anbi12d 632 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ∧ 𝑐 ∈ dom 𝐹) β†’ (((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ∧ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ (((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))))
204203rexbidva 3174 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆƒπ‘ ∈ dom 𝐹((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ∧ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ βˆƒπ‘ ∈ dom 𝐹(((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘) ∈ ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ ((◑𝐺 ∘ (π‘₯ ∘ 𝐹))β€˜π‘‘) = ((◑𝐺 ∘ (𝑦 ∘ 𝐹))β€˜π‘‘)))))
205112, 122, 2043bitr4rd 312 . . . . . . . . . . 11 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆƒπ‘ ∈ dom 𝐹((π‘₯β€˜(πΉβ€˜π‘))𝑆(π‘¦β€˜(πΉβ€˜π‘)) ∧ βˆ€π‘€ ∈ 𝐴 ((πΉβ€˜π‘)𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)))
20681, 85, 2053bitr3d 309 . . . . . . . . . 10 (((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) β†’ (βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)))
207206ex 414 . . . . . . . . 9 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ((π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ) β†’ (βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ↔ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦))))
208207pm5.32rd 579 . . . . . . . 8 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ((βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)) ↔ (((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))))
209208opabbidv 5176 . . . . . . 7 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))} = {⟨π‘₯, π‘¦βŸ© ∣ (((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))})
210 wemapwe.t . . . . . . . . 9 𝑇 = {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))}
211 df-xp 5644 . . . . . . . . 9 (π‘ˆ Γ— π‘ˆ) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)}
212210, 211ineq12i 4175 . . . . . . . 8 (𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) = ({⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))} ∩ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)})
213 inopab 5790 . . . . . . . 8 ({⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€)))} ∩ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)}) = {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))}
214212, 213eqtri 2765 . . . . . . 7 (𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) = {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘§ ∈ 𝐴 ((π‘₯β€˜π‘§)𝑆(π‘¦β€˜π‘§) ∧ βˆ€π‘€ ∈ 𝐴 (𝑧𝑅𝑀 β†’ (π‘₯β€˜π‘€) = (π‘¦β€˜π‘€))) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))}
215211ineq2i 4174 . . . . . . . 8 ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) = ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)})
216 inopab 5790 . . . . . . . 8 ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ)}) = {⟨π‘₯, π‘¦βŸ© ∣ (((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))}
217215, 216eqtri 2765 . . . . . . 7 ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) = {⟨π‘₯, π‘¦βŸ© ∣ (((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦) ∧ (π‘₯ ∈ π‘ˆ ∧ 𝑦 ∈ π‘ˆ))}
218209, 214, 2173eqtr4g 2802 . . . . . 6 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) = ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)))
219 weeq1 5626 . . . . . 6 ((𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) = ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) β†’ ((𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ ↔ ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ))
220218, 219syl 17 . . . . 5 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ ((𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ ↔ ({⟨π‘₯, π‘¦βŸ© ∣ ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘₯){βŸ¨π‘Ž, π‘βŸ© ∣ βˆƒπ‘ ∈ dom 𝐹((π‘Žβ€˜π‘) ∈ (π‘β€˜π‘) ∧ βˆ€π‘‘ ∈ dom 𝐹(𝑐 ∈ 𝑑 β†’ (π‘Žβ€˜π‘‘) = (π‘β€˜π‘‘)))} ((𝑓 ∈ π‘ˆ ↦ (◑𝐺 ∘ (𝑓 ∘ 𝐹)))β€˜π‘¦)} ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ))
22170, 220mpbird 257 . . . 4 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ (𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ)
222 weinxp 5721 . . . 4 (𝑇 We π‘ˆ ↔ (𝑇 ∩ (π‘ˆ Γ— π‘ˆ)) We π‘ˆ)
223221, 222sylibr 233 . . 3 ((πœ‘ ∧ (𝐡 ∈ V ∧ 𝐴 ∈ V)) β†’ 𝑇 We π‘ˆ)
224223ex 414 . 2 (πœ‘ β†’ ((𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ 𝑇 We π‘ˆ))
225 we0 5633 . . 3 𝑇 We βˆ…
226 elmapex 8793 . . . . . . . . 9 (π‘₯ ∈ (𝐡 ↑m 𝐴) β†’ (𝐡 ∈ V ∧ 𝐴 ∈ V))
227226con3i 154 . . . . . . . 8 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ Β¬ π‘₯ ∈ (𝐡 ↑m 𝐴))
228227pm2.21d 121 . . . . . . 7 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ (π‘₯ ∈ (𝐡 ↑m 𝐴) β†’ Β¬ π‘₯ finSupp 𝑍))
229228ralrimiv 3143 . . . . . 6 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ βˆ€π‘₯ ∈ (𝐡 ↑m 𝐴) Β¬ π‘₯ finSupp 𝑍)
230 rabeq0 4349 . . . . . 6 ({π‘₯ ∈ (𝐡 ↑m 𝐴) ∣ π‘₯ finSupp 𝑍} = βˆ… ↔ βˆ€π‘₯ ∈ (𝐡 ↑m 𝐴) Β¬ π‘₯ finSupp 𝑍)
231229, 230sylibr 233 . . . . 5 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ {π‘₯ ∈ (𝐡 ↑m 𝐴) ∣ π‘₯ finSupp 𝑍} = βˆ…)
2321, 231eqtrid 2789 . . . 4 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ π‘ˆ = βˆ…)
233 weeq2 5627 . . . 4 (π‘ˆ = βˆ… β†’ (𝑇 We π‘ˆ ↔ 𝑇 We βˆ…))
234232, 233syl 17 . . 3 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ (𝑇 We π‘ˆ ↔ 𝑇 We βˆ…))
235225, 234mpbiri 258 . 2 (Β¬ (𝐡 ∈ V ∧ 𝐴 ∈ V) β†’ 𝑇 We π‘ˆ)
236224, 235pm2.61d1 180 1 (πœ‘ β†’ 𝑇 We π‘ˆ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410  Vcvv 3448   ∩ cin 3914  βˆ…c0 4287   class class class wbr 5110  {copab 5172   ↦ cmpt 5193   E cep 5541   We wwe 5592   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638  ran crn 5639   ∘ ccom 5642  Ord word 6321  Oncon0 6322   Fn wfn 6496  βŸΆwf 6497  β€“1-1β†’wf1 6498  β€“ontoβ†’wfo 6499  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501   Isom wiso 6502  (class class class)co 7362   ↑o coe 8416   ↑m cmap 8772   finSupp cfsupp 9312  OrdIsocoi 9452   CNF ccnf 9604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-seqom 8399  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-oexp 8423  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-oi 9453  df-cnf 9605
This theorem is referenced by:  ltbwe  21461
  Copyright terms: Public domain W3C validator