Theorem wemapwe 8594

Description: Construct lexicographic order on a function space based on a reverse well-ordering of the indexes 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 2622	. . . . . . . . 9 ⊢ {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}
3		eqid 2622	. . . . . . . . 9 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘𝑍)
4		simprr 796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐴 ∈ V)
5		wemapwe.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 We 𝐴)
6	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑅 We 𝐴)
7		wemapwe.5	. . . . . . . . . . . 12 ⊢ 𝐹 = OrdIso(𝑅, 𝐴)
8	7	oiiso 8442	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
9	4, 6, 8	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
10		isof1o 6573	. . . . . . . . . 10 ⊢ (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴)
11	9, 10	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
12		simprl 794	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ∈ V)
13		wemapwe.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 We 𝐵)
14	13	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑆 We 𝐵)
15		wemapwe.6	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso(𝑆, 𝐵)
16	15	oiiso 8442	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝑆 We 𝐵) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
17	12, 14, 16	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
18		isof1o 6573	. . . . . . . . . 10 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → 𝐺:dom 𝐺–1-1-onto→𝐵)
19		f1ocnv 6149	. . . . . . . . . 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 8440	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → 𝐹 ∈ V)
22	21	ad2antll 765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 ∈ V)
23		dmexg 7097	. . . . . . . . . 10 ⊢ (𝐹 ∈ V → dom 𝐹 ∈ V)
24	22, 23	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ V)
25	15	oiexg 8440	. . . . . . . . . . 11 ⊢ (𝐵 ∈ V → 𝐺 ∈ V)
26	25	ad2antrl 764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 ∈ V)
27		dmexg 7097	. . . . . . . . . 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 6144	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → 𝐺:dom 𝐺–onto→𝐵)
32		forn 6118	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–onto→𝐵 → ran 𝐺 = 𝐵)
33	30, 31, 32	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 = 𝐵)
34		wemapwe.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ≠ ∅)
35	34	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ≠ ∅)
36	33, 35	eqnetrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 ≠ ∅)
37		dm0rn0 5342	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
38	37	necon3bii 2846	. . . . . . . . . . . . 13 ⊢ (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
39	36, 38	sylibr 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ≠ ∅)
40	15	oicl 8434	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
41		ord0eln0 5779	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 → (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅))
42	40, 41	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅)
43	39, 42	sylibr 224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ∅ ∈ dom 𝐺)
44	15	oif 8435	. . . . . . . . . . . 12 ⊢ 𝐺:dom 𝐺⟶𝐵
45	44	ffvelrni 6358	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ 𝐵)
46	43, 45	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝐺‘∅) ∈ 𝐵)
47	29, 46	syl5eqel 2705	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑍 ∈ 𝐵)
48	1, 2, 3, 11, 20, 4, 12, 24, 28, 47	mapfien 8313	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
49		eqid 2622	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅}
50	15	oion 8441	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → dom 𝐺 ∈ On)
51	50	ad2antrl 764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ On)
52	7	oion 8441	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom 𝐹 ∈ On)
53	52	ad2antll 765	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ On)
54	49, 51, 53	cantnfdm 8561	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅})
55	29	fveq2i 6194	. . . . . . . . . . . . 13 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘(𝐺‘∅))
56		f1ocnvfv1 6532	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺–1-1-onto→𝐵 ∧ ∅ ∈ dom 𝐺) → (◡𝐺‘(𝐺‘∅)) = ∅)
57	30, 43, 56	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘(𝐺‘∅)) = ∅)
58	55, 57	syl5eq 2668	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘𝑍) = ∅)
59	58	breq2d 4665	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑥 finSupp (◡𝐺‘𝑍) ↔ 𝑥 finSupp ∅))
60	59	rabbidv 3189	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp ∅})
61	54, 60	eqtr4d 2659	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑𝑚 dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
62		f1oeq3 6129	. . . . . . . . 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 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹))
65		eqid 2622	. . . . . . . . 9 ⊢ dom (dom 𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹)
66		eqid 2622	. . . . . . . . 9 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}
67	65, 51, 53, 66	oemapwe 8591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑𝑜 dom 𝐹)))
68	67	simpld 475	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹))
69		eqid 2622	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)}
70	69	f1owe 6603	. . . . . . 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 5186	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
73	71, 72	sylib 208	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
74	11	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
75		f1ofn 6138	. . . . . . . . . . . 12 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹 Fn dom 𝐹)
76		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑥‘𝑧) = (𝑥‘(𝐹‘𝑐)))
77		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑦‘𝑧) = (𝑦‘(𝐹‘𝑐)))
78	76, 77	breq12d 4666	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐))))
79		breq1 4656	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝑅𝑤 ↔ (𝐹‘𝑐)𝑅𝑤))
80	79	imbi1d 331	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
81	80	ralbidv 2986	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → (∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
82	78, 81	anbi12d 747	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑐) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
83	82	rexrn 6361	. . . . . . . . . . . 12 ⊢ (𝐹 Fn dom 𝐹 → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
84	74, 75, 83	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
85		f1ofo 6144	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴)
86		forn 6118	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴)
87	74, 85, 86	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ran 𝐹 = 𝐴)
88	87	rexeqdv 3145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
89	26	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐺 ∈ V)
90		cnvexg 7112	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ V → ◡𝐺 ∈ V)
91	89, 90	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ◡𝐺 ∈ V)
92		vex 3203	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
93	22	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹 ∈ V)
94		coexg 7117	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ V ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V)
95	92, 93, 94	sylancr 695	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥 ∘ 𝐹) ∈ V)
96		coexg 7117	. . . . . . . . . . . . . 14 ⊢ ((◡𝐺 ∈ V ∧ (𝑥 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
97	91, 95, 96	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
98		vex 3203	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
99		coexg 7117	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ V ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V)
100	98, 93, 99	sylancr 695	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∘ 𝐹) ∈ V)
101		coexg 7117	. . . . . . . . . . . . . 14 ⊢ ((◡𝐺 ∈ V ∧ (𝑦 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
102	91, 100, 101	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
103		fveq1 6190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐))
104		fveq1 6190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))
105		eleq12 2691	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∧ (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
106	103, 104, 105	syl2an 494	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
107		fveq1 6190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑑) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑))
108		fveq1 6190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))
109	107, 108	eqeqan12d 2638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑑) = (𝑏‘𝑑) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))
110	109	imbi2d 330	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ (𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
111	110	ralbidv 2986	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
112	106, 111	anbi12d 747	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
113	112	rexbidv 3052	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
114	113, 66	brabga 4989	. . . . . . . . . . . . 13 ⊢ (((◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
115	97, 102, 114	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
116		simprl 794	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
117		coeq1 5279	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑥 → (𝑓 ∘ 𝐹) = (𝑥 ∘ 𝐹))
118	117	coeq2d 5284	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑥 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
119		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))
120	118, 119	fvmptg 6280	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑈 ∧ (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
121	116, 97, 120	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
122		simprr 796	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
123		coeq1 5279	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑦 → (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹))
124	123	coeq2d 5284	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑦 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
125	124, 119	fvmptg 6280	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑈 ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
126	122, 102, 125	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
127	121, 126	breq12d 4666	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ↔ (◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹))))
128	17	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
129		isocnv 6580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
131		ssrab2 3687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} ⊆ (𝐵 ↑𝑚 𝐴)
132	1, 131	eqsstri 3635	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑈 ⊆ (𝐵 ↑𝑚 𝐴)
133	132, 116	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (𝐵 ↑𝑚 𝐴))
134		elmapi 7879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝐴) → 𝑥:𝐴⟶𝐵)
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥:𝐴⟶𝐵)
136	7	oif 8435	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹:dom 𝐹⟶𝐴
137	136	ffvelrni 6358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ dom 𝐹 → (𝐹‘𝑐) ∈ 𝐴)
138		ffvelrn 6357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
139	135, 137, 138	syl2an 494	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
140	132, 122	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (𝐵 ↑𝑚 𝐴))
141		elmapi 7879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝐵 ↑𝑚 𝐴) → 𝑦:𝐴⟶𝐵)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦:𝐴⟶𝐵)
143		ffvelrn 6357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
144	142, 137, 143	syl2an 494	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
145		isorel 6576	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺) ∧ ((𝑥‘(𝐹‘𝑐)) ∈ 𝐵 ∧ (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
146	130, 139, 144, 145	syl12anc 1324	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
147		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ∈ V
148	147	epelc 5031	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
149	146, 148	syl6bb 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
150	135	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑥:𝐴⟶𝐵)
151		fco 6058	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
152	150, 136, 151	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
153		fvco3 6275	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
154	152, 153	sylancom 701	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
155		simpr 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑐 ∈ dom 𝐹)
156		fvco3 6275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
157	136, 155, 156	sylancr 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
158	157	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
159	154, 158	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
160	142	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑦:𝐴⟶𝐵)
161		fco 6058	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
162	160, 136, 161	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
163		fvco3 6275	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
164	162, 163	sylancom 701	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
165		fvco3 6275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
166	136, 155, 165	sylancr 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
167	166	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
168	164, 167	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
169	159, 168	eleq12d 2695	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
170	149, 169	bitr4d 271	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
171	87	raleqdv 3144	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
172		breq2 4657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝐹‘𝑐)𝑅𝑤 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
173		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑑)))
174		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑑)))
175	173, 174	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
176	172, 175	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘𝑑) → (((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
177	176	ralrn 6362	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn dom 𝐹 → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
178	74, 75, 177	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
179	171, 178	bitr3d 270	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
180	179	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
181		epel 5032	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑)
182	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
183		isorel 6576	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
184	182, 183	sylancom 701	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
185	181, 184	syl5bbr 274	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 ∈ 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
186	152	adantrr 753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
187		simprr 796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝑑 ∈ dom 𝐹)
188		fvco3 6275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑑 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
189	186, 187, 188	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
190	162	adantrr 753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
191		fvco3 6275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑑 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
192	190, 187, 191	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
193	189, 192	eqeq12d 2637	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑))))
194	30	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
195		f1of1 6136	. . . . . . . . . . . . . . . . . . . . 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 6360	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵)
198	190, 187	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)
199		f1fveq 6519	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐺:𝐵–1-1→dom 𝐺 ∧ (((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵 ∧ ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
200	196, 197, 198, 199	syl12anc 1324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
201		fvco3 6275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
202	136, 187, 201	sylancr 695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
203		fvco3 6275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
204	136, 187, 203	sylancr 695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
205	202, 204	eqeq12d 2637	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
206	193, 200, 205	3bitrd 294	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
207	185, 206	imbi12d 334	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
208	207	anassrs 680	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
209	208	ralbidva 2985	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
210	180, 209	bitr4d 271	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
211	170, 210	anbi12d 747	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
212	211	rexbidva 3049	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
213	115, 127, 212	3bitr4rd 301	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
214	84, 88, 213	3bitr3d 298	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
215	214	ex 450	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))))
216	215	pm5.32rd 672	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ↔ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))))
217	216	opabbidv 4716	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))})
218		wemapwe.t	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
219		df-xp 5120	. . . . . . . . 9 ⊢ (𝑈 × 𝑈) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}
220	218, 219	ineq12i 3812	. . . . . . . 8 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
221		inopab 5252	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
222	220, 221	eqtri 2644	. . . . . . 7 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
223	219	ineq2i 3811	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
224		inopab 5252	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
225	223, 224	eqtri 2644	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
226	217, 222, 225	3eqtr4g 2681	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)))
227		weeq1 5102	. . . . . 6 ⊢ ((𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
228	226, 227	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
229	73, 228	mpbird 247	. . . 4 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
230		weinxp 5186	. . . 4 ⊢ (𝑇 We 𝑈 ↔ (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
231	229, 230	sylibr 224	. . 3 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑇 We 𝑈)
232	231	ex 450	. 2 ⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈))
233		we0 5109	. . 3 ⊢ 𝑇 We ∅
234		elmapex 7878	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝐴) → (𝐵 ∈ V ∧ 𝐴 ∈ V))
235	234	con3i 150	. . . . . . . 8 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ¬ 𝑥 ∈ (𝐵 ↑𝑚 𝐴))
236	235	pm2.21d 118	. . . . . . 7 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) → ¬ 𝑥 finSupp 𝑍))
237	236	ralrimiv 2965	. . . . . 6 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ∀𝑥 ∈ (𝐵 ↑𝑚 𝐴) ¬ 𝑥 finSupp 𝑍)
238		rabeq0 3957	. . . . . 6 ⊢ ({𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅ ↔ ∀𝑥 ∈ (𝐵 ↑𝑚 𝐴) ¬ 𝑥 finSupp 𝑍)
239	237, 238	sylibr 224	. . . . 5 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅)
240	1, 239	syl5eq 2668	. . . 4 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑈 = ∅)
241		weeq2 5103	. . . 4 ⊢ (𝑈 = ∅ → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
242	240, 241	syl 17	. . 3 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
243	233, 242	mpbiri 248	. 2 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈)
244	232, 243	pm2.61d1 171	1 ⊢ (𝜑 → 𝑇 We 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∩ cin 3573  ∅c0 3915   class class class wbr 4653  {copab 4712   ↦ cmpt 4729   E cep 5028   We wwe 5072   × cxp 5112  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   ∘ ccom 5118  Ord word 5722  Oncon0 5723   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –onto→wfo 5886  –1-1-onto→wf1o 5887  ‘cfv 5888   Isom wiso 5889  (class class class)co 6650   ↑_𝑜 coe 7559   ↑_𝑚 cmap 7857   finSupp cfsupp 8275  OrdIsocoi 8414   CNF ccnf 8558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seqom 7543  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-oexp 7566  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-cnf 8559

This theorem is referenced by:  ltbwe  19472