wemapwe - Metamath Proof Explorer

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

Theorem wemapwe 9694

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 2730	. . . . . . . . 9 ⊢ {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp (^◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp (^◡𝐺‘𝑍)}
3		eqid 2730	. . . . . . . . 9 ⊢ (^◡𝐺‘𝑍) = (^◡𝐺‘𝑍)
4		simprr 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐴 ∈ V)
5		wemapwe.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 We 𝐴)
6	5	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑅 We 𝐴)
7		wemapwe.5	. . . . . . . . . . . 12 ⊢ 𝐹 = OrdIso(𝑅, 𝐴)
8	7	oiiso 9534	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
9	4, 6, 8	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
10		isof1o 7322	. . . . . . . . . 10 ⊢ (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴)
11	9, 10	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
12		simprl 767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ∈ V)
13		wemapwe.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 We 𝐵)
14	13	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑆 We 𝐵)
15		wemapwe.6	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso(𝑆, 𝐵)
16	15	oiiso 9534	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝑆 We 𝐵) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
17	12, 14, 16	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
18		isof1o 7322	. . . . . . . . . 10 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → 𝐺:dom 𝐺–1-1-onto→𝐵)
19		f1ocnv 6844	. . . . . . . . . 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 9532	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → 𝐹 ∈ V)
22	21	ad2antll 725	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 ∈ V)
23	22	dmexd 7898	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ V)
24	15	oiexg 9532	. . . . . . . . . . 11 ⊢ (𝐵 ∈ V → 𝐺 ∈ V)
25	24	ad2antrl 724	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 ∈ V)
26	25	dmexd 7898	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ V)
27		wemapwe.7	. . . . . . . . . 10 ⊢ 𝑍 = (𝐺‘∅)
28	17, 18	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
29		f1ofo 6839	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → 𝐺:dom 𝐺–onto→𝐵)
30		forn 6807	. . . . . . . . . . . . . . 15 ⊢ (𝐺:dom 𝐺–onto→𝐵 → ran 𝐺 = 𝐵)
31	28, 29, 30	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 = 𝐵)
32		wemapwe.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ≠ ∅)
33	32	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ≠ ∅)
34	31, 33	eqnetrd 3006	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 ≠ ∅)
35		dm0rn0 5923	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
36	35	necon3bii 2991	. . . . . . . . . . . . 13 ⊢ (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
37	34, 36	sylibr 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ≠ ∅)
38	15	oicl 9526	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
39		ord0eln0 6418	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 → (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅))
40	38, 39	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 ↔ dom 𝐺 ≠ ∅)
41	37, 40	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ∅ ∈ dom 𝐺)
42	15	oif 9527	. . . . . . . . . . . 12 ⊢ 𝐺:dom 𝐺⟶𝐵
43	42	ffvelcdmi 7084	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ 𝐵)
44	41, 43	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝐺‘∅) ∈ 𝐵)
45	27, 44	eqeltrid 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑍 ∈ 𝐵)
46	1, 2, 3, 11, 20, 4, 12, 23, 26, 45	mapfien 9405	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp (^◡𝐺‘𝑍)})
47		eqid 2730	. . . . . . . . . . 11 ⊢ {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp ∅}
48	15	oion 9533	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → dom 𝐺 ∈ On)
49	48	ad2antrl 724	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ On)
50	7	oion 9533	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom 𝐹 ∈ On)
51	50	ad2antll 725	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ On)
52	47, 49, 51	cantnfdm 9661	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp ∅})
53	27	fveq2i 6893	. . . . . . . . . . . . 13 ⊢ (^◡𝐺‘𝑍) = (^◡𝐺‘(𝐺‘∅))
54		f1ocnvfv1 7276	. . . . . . . . . . . . . 14 ⊢ ((𝐺:dom 𝐺–1-1-onto→𝐵 ∧ ∅ ∈ dom 𝐺) → (^◡𝐺‘(𝐺‘∅)) = ∅)
55	28, 41, 54	syl2anc 582	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (^◡𝐺‘(𝐺‘∅)) = ∅)
56	53, 55	eqtrid 2782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (^◡𝐺‘𝑍) = ∅)
57	56	breq2d 5159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑥 finSupp (^◡𝐺‘𝑍) ↔ 𝑥 finSupp ∅))
58	57	rabbidv 3438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp (^◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp ∅})
59	52, 58	eqtr4d 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp (^◡𝐺‘𝑍)})
60	59	f1oeq3d 6829	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑_m dom 𝐹) ∣ 𝑥 finSupp (^◡𝐺‘𝑍)}))
61	46, 60	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom (dom 𝐺 CNF dom 𝐹))
62		eqid 2730	. . . . . . . . 9 ⊢ dom (dom 𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹)
63		eqid 2730	. . . . . . . . 9 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}
64	62, 49, 51, 63	oemapwe 9691	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑_o dom 𝐹)))
65	64	simpld 493	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹))
66		eqid 2730	. . . . . . . 8 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)}
67	66	f1owe 7352	. . . . . . 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 5759	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
70	68, 69	sylib 217	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)
71	11	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹:dom 𝐹–1-1-onto→𝐴)
72		f1ofn 6833	. . . . . . . . . . . 12 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹 Fn dom 𝐹)
73		fveq2 6890	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑥‘𝑧) = (𝑥‘(𝐹‘𝑐)))
74		fveq2 6890	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑦‘𝑧) = (𝑦‘(𝐹‘𝑐)))
75	73, 74	breq12d 5160	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐))))
76		breq1 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝑅𝑤 ↔ (𝐹‘𝑐)𝑅𝑤))
77	76	imbi1d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
78	77	ralbidv 3175	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑐) → (∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
79	75, 78	anbi12d 629	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑐) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
80	79	rexrn 7087	. . . . . . . . . . . 12 ⊢ (𝐹 Fn dom 𝐹 → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
81	71, 72, 80	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
82		f1ofo 6839	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴)
83		forn 6807	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴)
84	71, 82, 83	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ran 𝐹 = 𝐴)
85	84	rexeqdv 3324	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))))
86	25	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐺 ∈ V)
87		cnvexg 7917	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ V → ^◡𝐺 ∈ V)
88	86, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ^◡𝐺 ∈ V)
89		vex 3476	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
90	22	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹 ∈ V)
91		coexg 7922	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ V ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V)
92	89, 90, 91	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥 ∘ 𝐹) ∈ V)
93		coexg 7922	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 ∈ V ∧ (𝑥 ∘ 𝐹) ∈ V) → (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
94	88, 92, 93	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V)
95		vex 3476	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
96		coexg 7922	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ V ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V)
97	95, 90, 96	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∘ 𝐹) ∈ V)
98		coexg 7922	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 ∈ V ∧ (𝑦 ∘ 𝐹) ∈ V) → (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
99	88, 97, 98	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V)
100		fveq1 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑐) = ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐))
101		fveq1 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑐) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))
102		eleq12 2821	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑐) = ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∧ (𝑏‘𝑐) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
103	100, 101, 102	syl2an 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
104		fveq1 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑑) = ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑))
105		fveq1 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))
106	104, 105	eqeqan12d 2744	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑑) = (𝑏‘𝑑) ↔ ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))
107	106	imbi2d 339	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ (𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
108	107	ralbidv 3175	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
109	103, 108	anbi12d 629	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ (((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
110	109	rexbidv 3176	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (^◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ ∃𝑐 ∈ dom 𝐹(((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
111	110, 63	brabga 5533	. . . . . . . . . . . . 13 ⊢ (((^◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V ∧ (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
112	94, 99, 111	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (^◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
113		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))
114		coeq1 5856	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑥 → (𝑓 ∘ 𝐹) = (𝑥 ∘ 𝐹))
115	114	coeq2d 5861	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑥 → (^◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)))
116		simprl 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
117	113, 115, 116, 94	fvmptd3 7020	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (^◡𝐺 ∘ (𝑥 ∘ 𝐹)))
118		coeq1 5856	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑦 → (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹))
119	118	coeq2d 5861	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑦 → (^◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (^◡𝐺 ∘ (𝑦 ∘ 𝐹)))
120		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
121	113, 119, 120, 99	fvmptd3 7020	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (^◡𝐺 ∘ (𝑦 ∘ 𝐹)))
122	117, 121	breq12d 5160	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ↔ (^◡𝐺 ∘ (𝑥 ∘ 𝐹)){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (^◡𝐺 ∘ (𝑦 ∘ 𝐹))))
123	17	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵))
124		isocnv 7329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → ^◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
125	123, 124	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ^◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺))
126	1	ssrab3 4079	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑈 ⊆ (𝐵 ↑_m 𝐴)
127	126, 116	sselid 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (𝐵 ↑_m 𝐴))
128		elmapi 8845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐵 ↑_m 𝐴) → 𝑥:𝐴⟶𝐵)
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥:𝐴⟶𝐵)
130	7	oif 9527	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹:dom 𝐹⟶𝐴
131	130	ffvelcdmi 7084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ dom 𝐹 → (𝐹‘𝑐) ∈ 𝐴)
132		ffvelcdm 7082	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
133	129, 131, 132	syl2an 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵)
134	126, 120	sselid 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (𝐵 ↑_m 𝐴))
135		elmapi 8845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝐵 ↑_m 𝐴) → 𝑦:𝐴⟶𝐵)
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦:𝐴⟶𝐵)
137		ffvelcdm 7082	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
138	136, 131, 137	syl2an 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)
139		isorel 7325	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺) ∧ ((𝑥‘(𝐹‘𝑐)) ∈ 𝐵 ∧ (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (^◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (^◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
140	125, 133, 138, 139	syl12anc 833	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (^◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (^◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
141		fvex 6903	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐺‘(𝑦‘(𝐹‘𝑐))) ∈ V
142	141	epeli 5581	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (^◡𝐺‘(𝑦‘(𝐹‘𝑐))) ↔ (^◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (^◡𝐺‘(𝑦‘(𝐹‘𝑐))))
143	140, 142	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (^◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (^◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
144	129	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑥:𝐴⟶𝐵)
145		fco 6740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
146	144, 130, 145	sylancl 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
147		fvco3 6989	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
148	146, 147	sylancom 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)))
149		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑐 ∈ dom 𝐹)
150		fvco3 6989	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
151	130, 149, 150	sylancr 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐)))
152	151	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)) = (^◡𝐺‘(𝑥‘(𝐹‘𝑐))))
153	148, 152	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (^◡𝐺‘(𝑥‘(𝐹‘𝑐))))
154	136	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑦:𝐴⟶𝐵)
155		fco 6740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
156	154, 130, 155	sylancl 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
157		fvco3 6989	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
158	156, 157	sylancom 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)))
159		fvco3 6989	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
160	130, 149, 159	sylancr 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐)))
161	160	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)) = (^◡𝐺‘(𝑦‘(𝐹‘𝑐))))
162	158, 161	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (^◡𝐺‘(𝑦‘(𝐹‘𝑐))))
163	153, 162	eleq12d 2825	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ↔ (^◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (^◡𝐺‘(𝑦‘(𝐹‘𝑐)))))
164	143, 163	bitr4d 281	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)))
165	84	raleqdv 3323	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))
166		breq2 5151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝐹‘𝑐)𝑅𝑤 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
167		fveq2 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑑)))
168		fveq2 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝐹‘𝑑) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑑)))
169	167, 168	eqeq12d 2746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐹‘𝑑) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
170	166, 169	imbi12d 343	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝐹‘𝑑) → (((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
171	170	ralrn 7088	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn dom 𝐹 → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
172	71, 72, 171	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
173	165, 172	bitr3d 280	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
174	173	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
175		epel 5582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑)
176	9	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
177		isorel 7325	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
178	176, 177	sylancom 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
179	175, 178	bitr3id 284	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 ∈ 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑)))
180	146	adantrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵)
181		simprr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝑑 ∈ dom 𝐹)
182	180, 181	fvco3d 6990	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)))
183	156	adantrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵)
184	183, 181	fvco3d 6990	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))
185	182, 184	eqeq12d 2746	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑))))
186	28	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐺:dom 𝐺–1-1-onto→𝐵)
187		f1of1 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (^◡𝐺:𝐵–1-1-onto→dom 𝐺 → ^◡𝐺:𝐵–1-1→dom 𝐺)
188	186, 19, 187	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ^◡𝐺:𝐵–1-1→dom 𝐺)
189	180, 181	ffvelcdmd 7086	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵)
190	183, 181	ffvelcdmd 7086	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)
191		f1fveq 7263	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡𝐺:𝐵–1-1→dom 𝐺 ∧ (((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵 ∧ ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)) → ((^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
192	188, 189, 190, 191	syl12anc 833	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((^◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (^◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑)))
193		fvco3 6989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
194	130, 181, 193	sylancr 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑)))
195		fvco3 6989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
196	130, 181, 195	sylancr 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑)))
197	194, 196	eqeq12d 2746	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
198	185, 192, 197	3bitrd 304	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))
199	179, 198	imbi12d 343	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
200	199	anassrs 466	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) → ((𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
201	200	ralbidva 3173	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))))
202	174, 201	bitr4d 281	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))
203	164, 202	anbi12d 629	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ (((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
204	203	rexbidva 3174	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹(((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((^◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((^◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))))
205	112, 122, 204	3bitr4rd 311	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
206	81, 85, 205	3bitr3d 308	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))
207	206	ex 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))))
208	207	pm5.32rd 576	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ↔ (((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))))
209	208	opabbidv 5213	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))})
210		wemapwe.t	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
211		df-xp 5681	. . . . . . . . 9 ⊢ (𝑈 × 𝑈) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}
212	210, 211	ineq12i 4209	. . . . . . . 8 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
213		inopab 5828	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
214	212, 213	eqtri 2758	. . . . . . 7 ⊢ (𝑇 ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
215	211	ineq2i 4208	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)})
216		inopab 5828	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
217	215, 216	eqtri 2758	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = {⟨𝑥, 𝑦⟩ ∣ (((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}
218	209, 214, 217	3eqtr4g 2795	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)))
219		weeq1 5663	. . . . . 6 ⊢ ((𝑇 ∩ (𝑈 × 𝑈)) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
220	218, 219	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({⟨𝑥, 𝑦⟩ ∣ ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (^◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈))
221	70, 220	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
222		weinxp 5759	. . . 4 ⊢ (𝑇 We 𝑈 ↔ (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈)
223	221, 222	sylibr 233	. . 3 ⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑇 We 𝑈)
224	223	ex 411	. 2 ⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈))
225		we0 5670	. . 3 ⊢ 𝑇 We ∅
226		elmapex 8844	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑_m 𝐴) → (𝐵 ∈ V ∧ 𝐴 ∈ V))
227	226	con3i 154	. . . . . . . 8 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ¬ 𝑥 ∈ (𝐵 ↑_m 𝐴))
228	227	pm2.21d 121	. . . . . . 7 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐵 ↑_m 𝐴) → ¬ 𝑥 finSupp 𝑍))
229	228	ralrimiv 3143	. . . . . 6 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → ∀𝑥 ∈ (𝐵 ↑_m 𝐴) ¬ 𝑥 finSupp 𝑍)
230		rabeq0 4383	. . . . . 6 ⊢ ({𝑥 ∈ (𝐵 ↑_m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅ ↔ ∀𝑥 ∈ (𝐵 ↑_m 𝐴) ¬ 𝑥 finSupp 𝑍)
231	229, 230	sylibr 233	. . . . 5 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → {𝑥 ∈ (𝐵 ↑_m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅)
232	1, 231	eqtrid 2782	. . . 4 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑈 = ∅)
233		weeq2 5664	. . . 4 ⊢ (𝑈 = ∅ → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
234	232, 233	syl 17	. . 3 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑇 We 𝑈 ↔ 𝑇 We ∅))
235	225, 234	mpbiri 257	. 2 ⊢ (¬ (𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈)
236	224, 235	pm2.61d1 180	1 ⊢ (𝜑 → 𝑇 We 𝑈)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 {crab 3430 Vcvv 3472 ∩ cin 3946 ∅c0 4321 class class class wbr 5147 {copab 5209 ↦ cmpt 5230 E cep 5578 We wwe 5629 × cxp 5673 ^◡ccnv 5674 dom cdm 5675 ran crn 5676 ∘ ccom 5679 Ord word 6362 Oncon0 6363 Fn wfn 6537 ⟶wf 6538 –1-1→wf1 6539 –onto→wfo 6540 –1-1-onto→wf1o 6541 ‘cfv 6542 Isom wiso 6543 (class class class)co 7411 ↑_o coe 8467 ↑_m cmap 8822 finSupp cfsupp 9363 OrdIsocoi 9506 CNF ccnf 9658

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-seqom 8450 df-1o 8468 df-2o 8469 df-oadd 8472 df-omul 8473 df-oexp 8474 df-er 8705 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-oi 9507 df-cnf 9659

This theorem is referenced by: ltbwe 21818

W3C validator