Theorem wemapwe 9154

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 2821	. . . . . . . . 9 ⊢ {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}
3		eqid 2821	. . . . . . . . 9 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘𝑍)
4		simprr 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐴 ∈ V)
5		wemapwe.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 We 𝐴)
6	5	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑅 We 𝐴)
7		wemapwe.5	. . . . . . . . . . . 12 ⊢ 𝐹 = OrdIso(𝑅, 𝐴)
8	7	oiiso 8995	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
9	4, 6, 8	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
10		isof1o 7070	. . . . . . . . . 10 ⊢ (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴)
11	9, 10	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
12		simprl 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ∈ V)
13		wemapwe.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 We 𝐵)
14	13	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑆 We 𝐵)
15		wemapwe.6	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso(𝑆, 𝐵)
16	15	oiiso 8995	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝑆 We 𝐵) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
17	12, 14, 16	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
18		isof1o 7070	. . . . . . . . . 10 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → 𝐺:dom 𝐺–1-1-onto→𝐵)
19		f1ocnv 6622	. . . . . . . . . 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 8993	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → 𝐹 ∈ V)
22	21	ad2antll 727	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 ∈ V)
23	22	dmexd 7609	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ V)
24	15	oiexg 8993	. . . . . . . . . . 11 ⊢ (𝐵 ∈ V → 𝐺 ∈ V)
25	24	ad2antrl 726	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 ∈ V)
26	25	dmexd 7609	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ V)
27		wemapwe.7	. . . . . . . . . 10 ⊢ 𝑍 = (𝐺‘∅)
28	17, 18	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
29		f1ofo 6617	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → 𝐺:dom 𝐺–onto→𝐵)
30		forn 6588	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–onto→𝐵 → ran 𝐺 = 𝐵)
31	28, 29, 30	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 = 𝐵)
32		wemapwe.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ≠ ∅)
33	32	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ≠ ∅)
34	31, 33	eqnetrd 3083	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 ≠ ∅)
35		dm0rn0 5790	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
36	35	necon3bii 3068	. . . . . . . . . . . . 13 ⊢ (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
37	34, 36	sylibr 236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ≠ ∅)
38	15	oicl 8987	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
39		ord0eln0 6240	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 → (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅))
40	38, 39	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅)
41	37, 40	sylibr 236	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ∅ ∈ dom 𝐺)
42	15	oif 8988	. . . . . . . . . . . 12 ⊢ 𝐺:dom 𝐺⟶𝐵
43	42	ffvelrni 6845	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ 𝐵)
44	41, 43	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝐺‘∅) ∈ 𝐵)
45	27, 44	eqeltrid 2917	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑍 ∈ 𝐵)
46	1, 2, 3, 11, 20, 4, 12, 23, 26, 45	mapfien 8865	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
47		eqid 2821	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅}
48	15	oion 8994	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → dom 𝐺 ∈ On)
49	48	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ On)
50	7	oion 8994	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom 𝐹 ∈ On)
51	50	ad2antll 727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ On)
52	47, 49, 51	cantnfdm 9121	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅})
53	27	fveq2i 6668	. . . . . . . . . . . . 13 ⊢ (◡𝐺‘𝑍) = (◡𝐺‘(𝐺‘∅))
54		f1ocnvfv1 7027	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺–1-1-onto→𝐵 ∧ ∅ ∈ dom 𝐺) → (◡𝐺‘(𝐺‘∅)) = ∅)
55	28, 41, 54	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘(𝐺‘∅)) = ∅)
56	53, 55	syl5eq 2868	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘𝑍) = ∅)
57	56	breq2d 5071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑥 finSupp (◡𝐺‘𝑍) ↔ 𝑥 finSupp ∅))
58	57	rabbidv 3481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅})
59	52, 58	eqtr4d 2859	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})
60	59	f1oeq3d 6607	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}))
61	46, 60	mpbird 259	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹))
62		eqid 2821	. . . . . . . . 9 ⊢ dom (dom 𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹)
63		eqid 2821	. . . . . . . . 9 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}
64	62, 49, 51, 63	oemapwe 9151	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑o dom 𝐹)))
65	64	simpld 497	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹))
66		eqid 2821	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)}
67	66	f1owe 7100	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) → {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈))
68	61, 65, 67	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈)
69		weinxp 5631	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
70	68, 69	sylib 220	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
71	11	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
72		f1ofn 6611	. . . . . . . . . . . 12 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹 Fn dom 𝐹)
73		fveq2 6665	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑥‘𝑧) = (𝑥‘(𝐹‘𝑐)))
74		fveq2 6665	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑦‘𝑧) = (𝑦‘(𝐹‘𝑐)))
75	73, 74	breq12d 5072	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐))))
76		breq1 5062	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝑅𝑤 ↔ (𝐹‘𝑐)𝑅𝑤))
77	76	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
78	77	ralbidv 3197	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → (∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
79	75, 78	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑐) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
80	79	rexrn 6848	. . . . . . . . . . . 12 ⊢ (𝐹 Fn dom 𝐹 → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
81	71, 72, 80	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
82		f1ofo 6617	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴)
83		forn 6588	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴)
84	71, 82, 83	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ran 𝐹 = 𝐴)
85	84	rexeqdv 3417	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
86	25	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐺 ∈ V)
87		cnvexg 7623	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ V → ◡𝐺 ∈ V)
88	86, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ◡𝐺 ∈ V)
89		vex 3498	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
90	22	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹 ∈ V)
91		coexg 7628	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ V ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V)
92	89, 90, 91	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥 ∘ 𝐹) ∈ V)
93		coexg 7628	. . . . . . . . . . . . . 14 ⊢ ((◡𝐺 ∈ V ∧ (𝑥 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
94	88, 92, 93	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
95		vex 3498	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
96		coexg 7628	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ V ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V)
97	95, 90, 96	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∘ 𝐹) ∈ V)
98		coexg 7628	. . . . . . . . . . . . . 14 ⊢ ((◡𝐺 ∈ V ∧ (𝑦 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
99	88, 97, 98	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
100		fveq1 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐))
101		fveq1 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))
102		eleq12 2902	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∧ (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
103	100, 101, 102	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
104		fveq1 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑑) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑))
105		fveq1 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))
106	104, 105	eqeqan12d 2838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑑) = (𝑏‘𝑑) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))
107	106	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ (𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
108	107	ralbidv 3197	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
109	103, 108	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
110	109	rexbidv 3297	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
111	110, 63	brabga 5414	. . . . . . . . . . . . 13 ⊢ (((◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
112	94, 99, 111	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
113		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))
114		coeq1 5723	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑥 → (𝑓 ∘ 𝐹) = (𝑥 ∘ 𝐹))
115	114	coeq2d 5728	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑥 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
116		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
117	113, 115, 116, 94	fvmptd3 6786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹)))
118		coeq1 5723	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑦 → (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹))
119	118	coeq2d 5728	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑦 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
120		simprr 771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
121	113, 119, 120, 99	fvmptd3 6786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹)))
122	117, 121	breq12d 5072	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ↔ (◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹))))
123	17	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
124		isocnv 7077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
125	123, 124	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
126	1	ssrab3 4057	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)
127	126, 116	sseldi 3965	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (𝐵 ↑m 𝐴))
128		elmapi 8422	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐵 ↑m 𝐴) → 𝑥:𝐴⟶𝐵)
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥:𝐴⟶𝐵)
130	7	oif 8988	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹:dom 𝐹⟶𝐴
131	130	ffvelrni 6845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ dom 𝐹 → (𝐹‘𝑐) ∈ 𝐴)
132		ffvelrn 6844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
133	129, 131, 132	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
134	126, 120	sseldi 3965	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (𝐵 ↑m 𝐴))
135		elmapi 8422	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝐵 ↑m 𝐴) → 𝑦:𝐴⟶𝐵)
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦:𝐴⟶𝐵)
137		ffvelrn 6844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
138	136, 131, 137	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
139		isorel 7073	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺) ∧ ((𝑥‘(𝐹‘𝑐)) ∈ 𝐵 ∧ (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
140	125, 133, 138, 139	syl12anc 834	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
141		fvex 6678	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ∈ V
142	141	epeli 5463	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
143	140, 142	syl6bb 289	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
144	129	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑥:𝐴⟶𝐵)
145		fco 6526	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
146	144, 130, 145	sylancl 588	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
147		fvco3 6755	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
148	146, 147	sylancom 590	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
149		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑐 ∈ dom 𝐹)
150		fvco3 6755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
151	130, 149, 150	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
152	151	fveq2d 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
153	148, 152	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑥‘(𝐹‘𝑐))))
154	136	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑦:𝐴⟶𝐵)
155		fco 6526	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
156	154, 130, 155	sylancl 588	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
157		fvco3 6755	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
158	156, 157	sylancom 590	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
159		fvco3 6755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
160	130, 149, 159	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
161	160	fveq2d 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
162	158, 161	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑦‘(𝐹‘𝑐))))
163	153, 162	eleq12d 2907	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
164	143, 163	bitr4d 284	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
165	84	raleqdv 3416	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
166		breq2 5063	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝐹‘𝑐)𝑅𝑤 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
167		fveq2 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑑)))
168		fveq2 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑑)))
169	167, 168	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
170	166, 169	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘𝑑) → (((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
171	170	ralrn 6849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn dom 𝐹 → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
172	71, 72, 171	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
173	165, 172	bitr3d 283	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
174	173	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
175		epel 5464	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑)
176	9	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
177		isorel 7073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
178	176, 177	sylancom 590	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
179	175, 178	syl5bbr 287	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 ∈ 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
180	146	adantrr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
181		simprr 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝑑 ∈ dom 𝐹)
182		fvco3 6755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑑 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
183	180, 181, 182	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
184	156	adantrr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
185		fvco3 6755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑑 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
186	184, 181, 185	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
187	183, 186	eqeq12d 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑))))
188	28	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
189		f1of1 6609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐺:𝐵–1-1-onto→dom 𝐺 → ◡𝐺:𝐵–1-1→dom 𝐺)
190	188, 19, 189	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ◡𝐺:𝐵–1-1→dom 𝐺)
191	180, 181	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵)
192	184, 181	ffvelrnd 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)
193		f1fveq 7014	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐺:𝐵–1-1→dom 𝐺 ∧ (((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵 ∧ ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
194	190, 191, 192, 193	syl12anc 834	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
195		fvco3 6755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
196	130, 181, 195	sylancr 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
197		fvco3 6755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
198	130, 181, 197	sylancr 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
199	196, 198	eqeq12d 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
200	187, 194, 199	3bitrd 307	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
201	179, 200	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
202	201	anassrs 470	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
203	202	ralbidva 3196	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
204	174, 203	bitr4d 284	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
205	164, 204	anbi12d 632	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
206	205	rexbidva 3296	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
207	112, 122, 206	3bitr4rd 314	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
208	81, 85, 207	3bitr3d 311	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
209	208	ex 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))))
210	209	pm5.32rd 580	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ↔ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))))
211	210	opabbidv 5125	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))})
212		wemapwe.t	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
213		df-xp 5556	. . . . . . . . 9 ⊢ (𝑈 × 𝑈) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}
214	212, 213	ineq12i 4187	. . . . . . . 8 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
215		inopab 5696	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
216	214, 215	eqtri 2844	. . . . . . 7 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
217	213	ineq2i 4186	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
218		inopab 5696	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
219	217, 218	eqtri 2844	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
220	211, 216, 219	3eqtr4g 2881	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)))
221		weeq1 5538	. . . . . 6 ⊢ ((𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
222	220, 221	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
223	70, 222	mpbird 259	. . . 4 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
224		weinxp 5631	. . . 4 ⊢ (𝑇 We 𝑈 ↔ (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
225	223, 224	sylibr 236	. . 3 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑇 We 𝑈)
226	225	ex 415	. 2 ⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈))
227		we0 5545	. . 3 ⊢ 𝑇 We ∅
228		elmapex 8421	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑m 𝐴) → (𝐵 ∈ V ∧ 𝐴 ∈ V))
229	228	con3i 157	. . . . . . . 8 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ¬ 𝑥 ∈ (𝐵 ↑m 𝐴))
230	229	pm2.21d 121	. . . . . . 7 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐵 ↑m 𝐴) → ¬ 𝑥 finSupp 𝑍))
231	230	ralrimiv 3181	. . . . . 6 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ∀𝑥 ∈ (𝐵 ↑m 𝐴) ¬ 𝑥 finSupp 𝑍)
232		rabeq0 4338	. . . . . 6 ⊢ ({𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅ ↔ ∀𝑥 ∈ (𝐵 ↑m 𝐴) ¬ 𝑥 finSupp 𝑍)
233	231, 232	sylibr 236	. . . . 5 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅)
234	1, 233	syl5eq 2868	. . . 4 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑈 = ∅)
235		weeq2 5539	. . . 4 ⊢ (𝑈 = ∅ → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
236	234, 235	syl 17	. . 3 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
237	227, 236	mpbiri 260	. 2 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈)
238	226, 237	pm2.61d1 182	1 ⊢ (𝜑 → 𝑇 We 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3495   ∩ cin 3935  ∅c0 4291   class class class wbr 5059  {copab 5121   ↦ cmpt 5139   E cep 5459   We wwe 5508   × cxp 5548  ^◡ccnv 5549  dom cdm 5550  ran crn 5551   ∘ ccom 5554  Ord word 6185  Oncon0 6186   Fn wfn 6345  ⟶wf 6346  –1-1→wf1 6347  –onto→wfo 6348  –1-1-onto→wf1o 6349  ‘cfv 6350   Isom wiso 6351  (class class class)co 7150   ↑_o coe 8095   ↑_m cmap 8400   finSupp cfsupp 8827  OrdIsocoi 8967   CNF ccnf 9118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-se 5510  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-seqom 8078  df-1o 8096  df-2o 8097  df-oadd 8100  df-omul 8101  df-oexp 8102  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-oi 8968  df-cnf 9119

This theorem is referenced by:  ltbwe  20247