Theorem wemapwe 9664

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.

Step	Hyp	Ref	Expression
1		wemapwe.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}
2		eqid 2762	. . . . . . . . 9 ⊢ {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}
3		eqid 2762	. . . . . . . . 9 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘𝑍)
4		simprr 784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐴 ∈ V)
5		wemapwe.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 We 𝐴)
6	5	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑅 We 𝐴)
7		wemapwe.5	. . . . . . . . . . . 12 ⊢ 𝐹 = OrdIso(𝑅, 𝐴)
8	7	oiiso 9497	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
9	4, 6, 8	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
10		isof1o 7321	. . . . . . . . . 10 ⊢ (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴)
11	9, 10	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
12		simprl 782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ∈ V)
13		wemapwe.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 We 𝐵)
14	13	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑆 We 𝐵)
15		wemapwe.6	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso(𝑆, 𝐵)
16	15	oiiso 9497	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝑆 We 𝐵) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
17	12, 14, 16	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
18		isof1o 7321	. . . . . . . . . 10 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → 𝐺:dom 𝐺–1-1-onto→𝐵)
19		f1ocnv 6833	. . . . . . . . . 10 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→dom 𝐺)
20	17, 18, 19	3syl 19	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ◡𝐺:𝐵–1-1-onto→dom 𝐺)
21	7	oiexg 9495	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → 𝐹 ∈ V)
22	21	ad2antll 741	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 ∈ V)
23	22	dmexd 7898	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ V)
24	15	oiexg 9495	. . . . . . . . . . 11 ⊢ (𝐵 ∈ V → 𝐺 ∈ V)
25	24	ad2antrl 740	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 ∈ V)
26	25	dmexd 7898	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ V)
27		wemapwe.7	. . . . . . . . . 10 ⊢ 𝑍 = (𝐺‘∅)
28	17, 18	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
29		f1ofo 6828	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → 𝐺:dom 𝐺–onto→𝐵)
30		forn 6795	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–onto→𝐵 → ran 𝐺 = 𝐵)
31	28, 29, 30	3syl 19	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 = 𝐵)
32		wemapwe.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ≠ ∅)
33	32	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ≠ ∅)
34	31, 33	eqnetrd 3024	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 ≠ ∅)
35		dm0rn0 5913	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
36	35	necon3bii 3009	. . . . . . . . . . . . 13 ⊢ (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
37	34, 36	sylibr 237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ≠ ∅)
38	15	oicl 9489	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
39		ord0eln0 6417	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 → (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅))
40	38, 39	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅)
41	37, 40	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ∅ ∈ dom 𝐺)
42	15	oif 9490	. . . . . . . . . . . 12 ⊢ 𝐺:dom 𝐺⟶𝐵
43	42	ffvelcdmi 7078	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ 𝐵)
44	41, 43	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝐺‘∅) ∈ 𝐵)
45	27, 44	eqeltrid 2866	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑍 ∈ 𝐵)
46	1, 2, 3, 11, 20, 4, 12, 23, 26, 45	mapfien 9366	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
47		eqid 2762	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅}
48	15	oion 9496	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → dom 𝐺 ∈ On)
49	48	ad2antrl 740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ On)
50	7	oion 9496	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom 𝐹 ∈ On)
51	50	ad2antll 741	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ On)
52	47, 49, 51	cantnfdm 9631	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅})
53	27	fveq2i 6884	. . . . . . . . . . . . 13 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘(𝐺‘∅))
54		f1ocnvfv1 7274	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺–1-1-onto→𝐵 ∧ ∅ ∈ dom 𝐺) → (◡𝐺‘(𝐺‘∅)) = ∅)
55	28, 41, 54	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘(𝐺‘∅)) = ∅)
56	53, 55	eqtrid 2809	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘𝑍) = ∅)
57	56	breq2d 5120	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑥 finSupp (◡𝐺‘𝑍) ↔ 𝑥 finSupp ∅))
58	57	rabbidv 3422	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅})
59	52, 58	eqtr4d 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
60	59	f1oeq3d 6817	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}))
61	46, 60	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹))
62		eqid 2762	. . . . . . . . 9 ⊢ dom (dom 𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹)
63		eqid 2762	. . . . . . . . 9 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}
64	62, 49, 51, 63	oemapwe 9661	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑o dom 𝐹)))
65	64	simpld 499	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹))
66		eqid 2762	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)}
67	66	f1owe 7351	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) → ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹)))
68	67	biimprd 251	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) → {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈))
69	61, 65, 68	sylc 66	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈)
70		weinxp 5745	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
71	69, 70	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
72	11	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
73		f1ofn 6821	. . . . . . . . . . . 12 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹 Fn dom 𝐹)
74		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑥‘𝑧) = (𝑥‘(𝐹‘𝑐)))
75		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑦‘𝑧) = (𝑦‘(𝐹‘𝑐)))
76	74, 75	breq12d 5121	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐))))
77		breq1 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝑅𝑤 ↔ (𝐹‘𝑐)𝑅𝑤))
78	77	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
79	78	ralbidv 3187	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → (∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
80	76, 79	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑐) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
81	80	rexrn 7082	. . . . . . . . . . . 12 ⊢ (𝐹 Fn dom 𝐹 → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
82	72, 73, 81	3syl 19	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
83		f1ofo 6828	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴)
84		forn 6795	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴)
85	72, 83, 84	3syl 19	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ran 𝐹 = 𝐴)
86	85	rexeqdv 3323	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
87	25	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐺 ∈ V)
88		cnvexg 7919	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ V → ◡𝐺 ∈ V)
89	87, 88	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ◡𝐺 ∈ V)
90		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
91	22	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹 ∈ V)
92		coexg 7924	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ V ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V)
93	90, 91, 92	sylancr 598	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥 ∘ 𝐹) ∈ V)
94	89, 93	coexd 7926	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
95		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
96		coexg 7924	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ V ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V)
97	95, 91, 96	sylancr 598	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∘ 𝐹) ∈ V)
98	89, 97	coexd 7926	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
99		fveq1 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐))
100		fveq1 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))
101		eleq12 2852	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∧ (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
102	99, 100, 101	syl2an 607	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
103		fveq1 6880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑑) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑))
104		fveq1 6880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))
105	103, 104	eqeqan12d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑑) = (𝑏‘𝑑) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))
106	105	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ (𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
107	106	ralbidv 3187	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
108	102, 107	anbi12d 643	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
109	108	rexbidv 3188	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
110	109, 63	brabga 5517	. . . . . . . . . . . . 13 ⊢ (((◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
111	94, 98, 110	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
112		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))
113		coeq1 5842	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑥 → (𝑓 ∘ 𝐹) = (𝑥 ∘ 𝐹))
114	113	coeq2d 5847	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑥 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
115		simprl 782	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
116	112, 114, 115, 94	fvmptd3 7013	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
117		coeq1 5842	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑦 → (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹))
118	117	coeq2d 5847	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑦 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
119		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
120	112, 118, 119, 98	fvmptd3 7013	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
121	116, 120	breq12d 5121	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ↔ (◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹))))
122	17	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
123		isocnv 7328	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
124	122, 123	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
125	1	ssrab3 4035	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)
126	125, 115	sselid 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (𝐵 ↑m 𝐴))
127		elmapi 8844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐵 ↑m 𝐴) → 𝑥:𝐴⟶𝐵)
128	126, 127	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥:𝐴⟶𝐵)
129	7	oif 9490	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹:dom 𝐹⟶𝐴
130	129	ffvelcdmi 7078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ dom 𝐹 → (𝐹‘𝑐) ∈ 𝐴)
131		ffvelcdm 7076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
132	128, 130, 131	syl2an 607	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
133	125, 119	sselid 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (𝐵 ↑m 𝐴))
134		elmapi 8844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝐵 ↑m 𝐴) → 𝑦:𝐴⟶𝐵)
135	133, 134	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦:𝐴⟶𝐵)
136		ffvelcdm 7076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
137	135, 130, 136	syl2an 607	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
138		isorel 7324	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺) ∧ ((𝑥‘(𝐹‘𝑐)) ∈ 𝐵 ∧ (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
139	124, 132, 137, 138	syl12anc 849	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
140		fvex 6894	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ∈ V
141	140	epeli 5562	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
142	139, 141	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
143	128	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑥:𝐴⟶𝐵)
144		fco 6730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
145	143, 129, 144	sylancl 597	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
146		fvco3 6981	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
147	145, 146	sylancom 599	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
148		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑐 ∈ dom 𝐹)
149		fvco3 6981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
150	129, 148, 149	sylancr 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
151	150	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
152	147, 151	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
153	135	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑦:𝐴⟶𝐵)
154		fco 6730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
155	153, 129, 154	sylancl 597	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
156		fvco3 6981	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
157	155, 156	sylancom 599	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
158		fvco3 6981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
159	129, 148, 158	sylancr 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
160	159	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
161	157, 160	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
162	152, 161	eleq12d 2856	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
163	142, 162	bitr4d 285	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
164	85	raleqdv 3322	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
165		breq2 5112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝐹‘𝑐)𝑅𝑤 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
166		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑑)))
167		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑑)))
168	166, 167	eqeq12d 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
169	165, 168	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘𝑑) → (((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
170	169	ralrn 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn dom 𝐹 → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
171	72, 73, 170	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
172	164, 171	bitr3d 284	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
173	172	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
174		epel 5563	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑)
175	9	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
176		isorel 7324	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
177	175, 176	sylancom 599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
178	174, 177	bitr3id 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 ∈ 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
179	145	adantrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
180		simprr 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝑑 ∈ dom 𝐹)
181	179, 180	fvco3d 6982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
182	155	adantrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
183	182, 180	fvco3d 6982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
184	181, 183	eqeq12d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑))))
185	28	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
186		f1of1 6819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐺:𝐵–1-1-onto→dom 𝐺 → ◡𝐺:𝐵–1-1→dom 𝐺)
187	185, 19, 186	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ◡𝐺:𝐵–1-1→dom 𝐺)
188	179, 180	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵)
189	182, 180	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)
190		f1fveq 7260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐺:𝐵–1-1→dom 𝐺 ∧ (((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵 ∧ ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
191	187, 188, 189, 190	syl12anc 849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
192		fvco3 6981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
193	129, 180, 192	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
194		fvco3 6981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
195	129, 180, 194	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
196	193, 195	eqeq12d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
197	184, 191, 196	3bitrd 308	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
198	178, 197	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
199	198	anassrs 472	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
200	199	ralbidva 3185	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
201	173, 200	bitr4d 285	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
202	163, 201	anbi12d 643	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
203	202	rexbidva 3186	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
204	111, 121, 203	3bitr4rd 315	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
205	82, 86, 204	3bitr3d 312	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
206	205	ex 417	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))))
207	206	pm5.32rd 588	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ↔ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))))
208	207	opabbidv 5176	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))})
209		wemapwe.t	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
210		df-xp 5666	. . . . . . . . 9 ⊢ (𝑈 × 𝑈) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}
211	209, 210	ineq12i 4170	. . . . . . . 8 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
212		inopab 5815	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
213	211, 212	eqtri 2785	. . . . . . 7 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
214	210	ineq2i 4169	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
215		inopab 5815	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
216	214, 215	eqtri 2785	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
217	208, 213, 216	3eqtr4g 2822	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)))
218		weeq1 5647	. . . . . 6 ⊢ ((𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
219	217, 218	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
220	71, 219	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
221		weinxp 5745	. . . 4 ⊢ (𝑇 We 𝑈 ↔ (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
222	220, 221	sylibr 237	. . 3 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑇 We 𝑈)
223	222	ex 417	. 2 ⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈))
224		we0 5655	. . 3 ⊢ 𝑇 We ∅
225		elmapex 8843	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑m 𝐴) → (𝐵 ∈ V ∧ 𝐴 ∈ V))
226	225	con3i 155	. . . . . . . 8 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ¬ 𝑥 ∈ (𝐵 ↑m 𝐴))
227	226	pm2.21d 122	. . . . . . 7 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐵 ↑m 𝐴) → ¬ 𝑥 finSupp 𝑍))
228	227	ralrimiv 3155	. . . . . 6 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ∀𝑥 ∈ (𝐵 ↑m 𝐴) ¬ 𝑥 finSupp 𝑍)
229		rabeq0 4344	. . . . . 6 ⊢ ({𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅ ↔ ∀𝑥 ∈ (𝐵 ↑m 𝐴) ¬ 𝑥 finSupp 𝑍)
230	228, 229	sylibr 237	. . . . 5 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅)
231	1, 230	eqtrid 2809	. . . 4 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑈 = ∅)
232		weeq2 5648	. . . 4 ⊢ (𝑈 = ∅ → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
233	231, 232	syl 18	. . 3 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
234	224, 233	mpbiri 261	. 2 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈)
235	223, 234	pm2.61d1 182	1 ⊢ (𝜑 → 𝑇 We 𝑈)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569   ∈ wcel 2142   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3415  Vcvv 3454   ∩ cin 3903  ∅c0 4285   class class class wbr 5108  {copab 5172   ↦ cmpt 5191   E cep 5559   We wwe 5612   × cxp 5658  ^◡ccnv 5659  dom cdm 5660  ran crn 5661   ∘ ccom 5664  Ord word 6359  Oncon0 6360   Fn wfn 6531  ⟶wf 6532  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536   Isom wiso 6537  (class class class)co 7412   ↑_o coe 8450   ↑_m cmap 8822   finSupp cfsupp 9319  OrdIsocoi 9469   CNF ccnf 9628

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-se 5614  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-supp 8155  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-seqom 8433  df-1o 8451  df-2o 8452  df-oadd 8455  df-omul 8456  df-oexp 8457  df-er 8692  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9320  df-oi 9470  df-cnf 9629

This theorem is used by:  ltbwe  22206