Theorem wemapwe 8851

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	⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 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.

Step	Hyp	Ref	Expression
1		wemapwe.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍}
2		eqid 2817	. . . . . . . . 9 ⊢ {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}
3		eqid 2817	. . . . . . . . 9 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘𝑍)
4		simprr 780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐴 ∈ V)
5		wemapwe.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 We 𝐴)
6	5	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑅 We 𝐴)
7		wemapwe.5	. . . . . . . . . . . 12 ⊢ 𝐹 = OrdIso(𝑅, 𝐴)
8	7	oiiso 8691	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
9	4, 6, 8	syl2anc 575	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
10		isof1o 6807	. . . . . . . . . 10 ⊢ (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴)
11	9, 10	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
12		simprl 778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ∈ V)
13		wemapwe.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 We 𝐵)
14	13	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑆 We 𝐵)
15		wemapwe.6	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso(𝑆, 𝐵)
16	15	oiiso 8691	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝑆 We 𝐵) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
17	12, 14, 16	syl2anc 575	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
18		isof1o 6807	. . . . . . . . . 10 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → 𝐺:dom 𝐺–1-1-onto→𝐵)
19		f1ocnv 6375	. . . . . . . . . 10 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→dom 𝐺)
20	17, 18, 19	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ◡𝐺:𝐵–1-1-onto→dom 𝐺)
21	7	oiexg 8689	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → 𝐹 ∈ V)
22	21	ad2antll 711	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 ∈ V)
23		dmexg 7337	. . . . . . . . . 10 ⊢ (𝐹 ∈ V → dom 𝐹 ∈ V)
24	22, 23	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ V)
25	15	oiexg 8689	. . . . . . . . . . 11 ⊢ (𝐵 ∈ V → 𝐺 ∈ V)
26	25	ad2antrl 710	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 ∈ V)
27		dmexg 7337	. . . . . . . . . 10 ⊢ (𝐺 ∈ V → dom 𝐺 ∈ V)
28	26, 27	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ V)
29		wemapwe.7	. . . . . . . . . 10 ⊢ 𝑍 = (𝐺‘∅)
30	17, 18	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
31		f1ofo 6370	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → 𝐺:dom 𝐺–onto→𝐵)
32		forn 6344	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–onto→𝐵 → ran 𝐺 = 𝐵)
33	30, 31, 32	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 = 𝐵)
34		wemapwe.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ≠ ∅)
35	34	adantr 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ≠ ∅)
36	33, 35	eqnetrd 3056	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 ≠ ∅)
37		dm0rn0 5557	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
38	37	necon3bii 3041	. . . . . . . . . . . . 13 ⊢ (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
39	36, 38	sylibr 225	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ≠ ∅)
40	15	oicl 8683	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
41		ord0eln0 6005	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 → (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅))
42	40, 41	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅)
43	39, 42	sylibr 225	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ∅ ∈ dom 𝐺)
44	15	oif 8684	. . . . . . . . . . . 12 ⊢ 𝐺:dom 𝐺⟶𝐵
45	44	ffvelrni 6590	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ 𝐵)
46	43, 45	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝐺‘∅) ∈ 𝐵)
47	29, 46	syl5eqel 2900	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑍 ∈ 𝐵)
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 8562	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
49		eqid 2817	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅}
50	15	oion 8690	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → dom 𝐺 ∈ On)
51	50	ad2antrl 710	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ On)
52	7	oion 8690	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom 𝐹 ∈ On)
53	52	ad2antll 711	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ On)
54	49, 51, 53	cantnfdm 8818	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅})
55	29	fveq2i 6421	. . . . . . . . . . . . 13 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘(𝐺‘∅))
56		f1ocnvfv1 6766	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺–1-1-onto→𝐵 ∧ ∅ ∈ dom 𝐺) → (◡𝐺‘(𝐺‘∅)) = ∅)
57	30, 43, 56	syl2anc 575	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘(𝐺‘∅)) = ∅)
58	55, 57	syl5eq 2863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘𝑍) = ∅)
59	58	breq2d 4867	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑥 finSupp (◡𝐺‘𝑍) ↔ 𝑥 finSupp ∅))
60	59	rabbidv 3390	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅})
61	54, 60	eqtr4d 2854	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
62		f1oeq3 6355	. . . . . . . . 9 ⊢ (dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}))
63	61, 62	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}))
64	48, 63	mpbird 248	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹))
65		eqid 2817	. . . . . . . . 9 ⊢ dom (dom 𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹)
66		eqid 2817	. . . . . . . . 9 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}
67	65, 51, 53, 66	oemapwe 8848	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑𝑜 dom 𝐹)))
68	67	simpld 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹))
69		eqid 2817	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)}
70	69	f1owe 6837	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) → {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈))
71	64, 68, 70	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈)
72		weinxp 5402	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
73	71, 72	sylib 209	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
74	11	adantr 468	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
75		f1ofn 6364	. . . . . . . . . . . 12 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹 Fn dom 𝐹)
76		fveq2 6418	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑥‘𝑧) = (𝑥‘(𝐹‘𝑐)))
77		fveq2 6418	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑦‘𝑧) = (𝑦‘(𝐹‘𝑐)))
78	76, 77	breq12d 4868	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐))))
79		breq1 4858	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝑅𝑤 ↔ (𝐹‘𝑐)𝑅𝑤))
80	79	imbi1d 332	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
81	80	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → (∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
82	78, 81	anbi12d 618	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑐) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
83	82	rexrn 6593	. . . . . . . . . . . 12 ⊢ (𝐹 Fn dom 𝐹 → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
84	74, 75, 83	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
85		f1ofo 6370	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴)
86		forn 6344	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴)
87	74, 85, 86	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ran 𝐹 = 𝐴)
88	87	rexeqdv 3345	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
89	26	adantr 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐺 ∈ V)
90		cnvexg 7352	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ V → ◡𝐺 ∈ V)
91	89, 90	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ◡𝐺 ∈ V)
92		vex 3405	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
93	22	adantr 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹 ∈ V)
94		coexg 7357	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ V ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V)
95	92, 93, 94	sylancr 577	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥 ∘ 𝐹) ∈ V)
96		coexg 7357	. . . . . . . . . . . . . 14 ⊢ ((◡𝐺 ∈ V ∧ (𝑥 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
97	91, 95, 96	syl2anc 575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
98		vex 3405	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
99		coexg 7357	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ V ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V)
100	98, 93, 99	sylancr 577	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∘ 𝐹) ∈ V)
101		coexg 7357	. . . . . . . . . . . . . 14 ⊢ ((◡𝐺 ∈ V ∧ (𝑦 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
102	91, 100, 101	syl2anc 575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
103		fveq1 6417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐))
104		fveq1 6417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))
105		eleq12 2886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∧ (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
106	103, 104, 105	syl2an 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
107		fveq1 6417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑑) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑))
108		fveq1 6417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))
109	107, 108	eqeqan12d 2833	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑑) = (𝑏‘𝑑) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))
110	109	imbi2d 331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ (𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
111	110	ralbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
112	106, 111	anbi12d 618	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
113	112	rexbidv 3251	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
114	113, 66	brabga 5197	. . . . . . . . . . . . 13 ⊢ (((◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
115	97, 102, 114	syl2anc 575	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
116		simprl 778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
117		coeq1 5495	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑥 → (𝑓 ∘ 𝐹) = (𝑥 ∘ 𝐹))
118	117	coeq2d 5500	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑥 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
119		eqid 2817	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))
120	118, 119	fvmptg 6511	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑈 ∧ (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
121	116, 97, 120	syl2anc 575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
122		simprr 780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
123		coeq1 5495	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑦 → (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹))
124	123	coeq2d 5500	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑦 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
125	124, 119	fvmptg 6511	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑈 ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
126	122, 102, 125	syl2anc 575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
127	121, 126	breq12d 4868	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ↔ (◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹))))
128	17	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
129		isocnv 6814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
131		ssrab2 3895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} ⊆ (𝐵 ↑𝑚 𝐴)
132	1, 131	eqsstri 3843	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑈 ⊆ (𝐵 ↑𝑚 𝐴)
133	132, 116	sseldi 3807	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (𝐵 ↑𝑚 𝐴))
134		elmapi 8124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝐴) → 𝑥:𝐴⟶𝐵)
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥:𝐴⟶𝐵)
136	7	oif 8684	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹:dom 𝐹⟶𝐴
137	136	ffvelrni 6590	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ dom 𝐹 → (𝐹‘𝑐) ∈ 𝐴)
138		ffvelrn 6589	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
139	135, 137, 138	syl2an 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
140	132, 122	sseldi 3807	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (𝐵 ↑𝑚 𝐴))
141		elmapi 8124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝐵 ↑𝑚 𝐴) → 𝑦:𝐴⟶𝐵)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦:𝐴⟶𝐵)
143		ffvelrn 6589	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
144	142, 137, 143	syl2an 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
145		isorel 6810	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺) ∧ ((𝑥‘(𝐹‘𝑐)) ∈ 𝐵 ∧ (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
146	130, 139, 144, 145	syl12anc 856	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
147		fvex 6431	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ∈ V
148	147	epeli 5239	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
149	146, 148	syl6bb 278	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
150	135	adantr 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑥:𝐴⟶𝐵)
151		fco 6283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
152	150, 136, 151	sylancl 576	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
153		fvco3 6506	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
154	152, 153	sylancom 578	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
155		simpr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑐 ∈ dom 𝐹)
156		fvco3 6506	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
157	136, 155, 156	sylancr 577	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
158	157	fveq2d 6422	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
159	154, 158	eqtrd 2851	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
160	142	adantr 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑦:𝐴⟶𝐵)
161		fco 6283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
162	160, 136, 161	sylancl 576	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
163		fvco3 6506	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
164	162, 163	sylancom 578	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
165		fvco3 6506	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
166	136, 155, 165	sylancr 577	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
167	166	fveq2d 6422	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
168	164, 167	eqtrd 2851	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
169	159, 168	eleq12d 2890	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
170	149, 169	bitr4d 273	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
171	87	raleqdv 3344	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
172		breq2 4859	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝐹‘𝑐)𝑅𝑤 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
173		fveq2 6418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑑)))
174		fveq2 6418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑑)))
175	173, 174	eqeq12d 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
176	172, 175	imbi12d 335	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘𝑑) → (((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
177	176	ralrn 6594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn dom 𝐹 → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
178	74, 75, 177	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
179	171, 178	bitr3d 272	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
180	179	adantr 468	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
181		epel 5240	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑)
182	9	ad2antrr 708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
183		isorel 6810	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
184	182, 183	sylancom 578	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
185	181, 184	syl5bbr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 ∈ 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
186	152	adantrr 699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
187		simprr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝑑 ∈ dom 𝐹)
188		fvco3 6506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑑 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
189	186, 187, 188	syl2anc 575	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
190	162	adantrr 699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
191		fvco3 6506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑑 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
192	190, 187, 191	syl2anc 575	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
193	189, 192	eqeq12d 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑))))
194	30	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
195		f1of1 6362	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐺:𝐵–1-1-onto→dom 𝐺 → ◡𝐺:𝐵–1-1→dom 𝐺)
196	194, 19, 195	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ◡𝐺:𝐵–1-1→dom 𝐺)
197	186, 187	ffvelrnd 6592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵)
198	190, 187	ffvelrnd 6592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)
199		f1fveq 6753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐺:𝐵–1-1→dom 𝐺 ∧ (((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵 ∧ ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
200	196, 197, 198, 199	syl12anc 856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
201		fvco3 6506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
202	136, 187, 201	sylancr 577	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
203		fvco3 6506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
204	136, 187, 203	sylancr 577	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
205	202, 204	eqeq12d 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
206	193, 200, 205	3bitrd 296	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
207	185, 206	imbi12d 335	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
208	207	anassrs 455	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
209	208	ralbidva 3184	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
210	180, 209	bitr4d 273	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
211	170, 210	anbi12d 618	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
212	211	rexbidva 3248	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
213	115, 127, 212	3bitr4rd 303	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
214	84, 88, 213	3bitr3d 300	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
215	214	ex 399	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))))
216	215	pm5.32rd 569	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ↔ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))))
217	216	opabbidv 4921	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))})
218		wemapwe.t	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
219		df-xp 5330	. . . . . . . . 9 ⊢ (𝑈 × 𝑈) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}
220	218, 219	ineq12i 4022	. . . . . . . 8 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
221		inopab 5468	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
222	220, 221	eqtri 2839	. . . . . . 7 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
223	219	ineq2i 4021	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
224		inopab 5468	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
225	223, 224	eqtri 2839	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
226	217, 222, 225	3eqtr4g 2876	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)))
227		weeq1 5312	. . . . . 6 ⊢ ((𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
228	226, 227	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
229	73, 228	mpbird 248	. . . 4 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
230		weinxp 5402	. . . 4 ⊢ (𝑇 We 𝑈 ↔ (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
231	229, 230	sylibr 225	. . 3 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑇 We 𝑈)
232	231	ex 399	. 2 ⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈))
233		we0 5319	. . 3 ⊢ 𝑇 We ∅
234		elmapex 8123	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝐴) → (𝐵 ∈ V ∧ 𝐴 ∈ V))
235	234	con3i 151	. . . . . . . 8 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ¬ 𝑥 ∈ (𝐵 ↑𝑚 𝐴))
236	235	pm2.21d 119	. . . . . . 7 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) → ¬ 𝑥 finSupp 𝑍))
237	236	ralrimiv 3164	. . . . . 6 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ∀𝑥 ∈ (𝐵 ↑𝑚 𝐴) ¬ 𝑥 finSupp 𝑍)
238		rabeq0 4168	. . . . . 6 ⊢ ({𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅ ↔ ∀𝑥 ∈ (𝐵 ↑𝑚 𝐴) ¬ 𝑥 finSupp 𝑍)
239	237, 238	sylibr 225	. . . . 5 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅)
240	1, 239	syl5eq 2863	. . . 4 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑈 = ∅)
241		weeq2 5313	. . . 4 ⊢ (𝑈 = ∅ → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
242	240, 241	syl 17	. . 3 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
243	233, 242	mpbiri 249	. 2 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈)
244	232, 243	pm2.61d1 172	1 ⊢ (𝜑 → 𝑇 We 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2157   ≠ wne 2989  ∀wral 3107  ∃wrex 3108  {crab 3111  Vcvv 3402   ∩ cin 3779  ∅c0 4127   class class class wbr 4855  {copab 4917   ↦ cmpt 4934   E cep 5236   We wwe 5282   × cxp 5322  ^◡ccnv 5323  dom cdm 5324  ran crn 5325   ∘ ccom 5328  Ord word 5949  Oncon0 5950   Fn wfn 6106  ⟶wf 6107  –1-1→wf1 6108  –onto→wfo 6109  –1-1-onto→wf1o 6110  ‘cfv 6111   Isom wiso 6112  (class class class)co 6884   ↑_𝑜 coe 7805   ↑_𝑚 cmap 8102   finSupp cfsupp 8524  OrdIsocoi 8663   CNF ccnf 8815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-seqom 7789  df-1o 7806  df-2o 7807  df-oadd 7810  df-omul 7811  df-oexp 7812  df-er 7989  df-map 8104  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-oi 8664  df-cnf 8816

This theorem is referenced by:  ltbwe  19701