Theorem elfuns 36413

Description: Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)

Hypothesis

Ref	Expression
elfuns.1	⊢ 𝐹 ∈ V

Assertion

Ref	Expression
elfuns	⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)

Proof of Theorem elfuns

Dummy variables 𝑎 𝑥 𝑦 𝑧 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrel 5783	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑝 ∈ 𝐹) → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
2	1	ex 417	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑝 ∈ 𝐹 → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3		elrel 5783	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑞 ∈ 𝐹) → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
4	3	ex 417	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑞 ∈ 𝐹 → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
5	2, 4	anim12d 620	. . . . . . . . 9 ⊢ (Rel 𝐹 → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
6	5	adantrd 496	. . . . . . . 8 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
7	6	pm4.71rd 571	. . . . . . 7 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8		19.41vvvv 1981	. . . . . . . 8 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9		ee4anv 2382	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
10	9	anbi1i 635	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
11	8, 10	bitr2i 279	. . . . . . 7 ⊢ (((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
12	7, 11	bitrdi 290	. . . . . 6 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13	12	2exbidv 1953	. . . . 5 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14		excom13 2198	. . . . . 6 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15		excom13 2198	. . . . . . . 8 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16		exrot4 2200	. . . . . . . . . 10 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17		excom 2196	. . . . . . . . . 10 ⊢ (∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18		df-3an 1104	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19	18	2exbii 1878	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20		opex 5444	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
21		opex 5444	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑧⟩ ∈ V
22		eleq1 2850	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
23	22	anbi1d 642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹)))
24		breq2 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
25	23, 24	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26		eleq1 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞 ∈ 𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
27	26	anbi2d 641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28		breq1 5111	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29		vex 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
30		vex 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
31	21, 29, 30	brtxp 36378	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32		vex 3458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
33		vex 3458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
34	32, 33	br1steq 36271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑥 = 𝑎)
35		equcom 2047	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 ↔ 𝑎 = 𝑥)
36	34, 35	bitri 278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑎 = 𝑥)
37	21, 30	brco 5855	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦))
38	32, 33	br2ndeq 36272	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑧⟩2nd 𝑥 ↔ 𝑥 = 𝑧)
39	38	anbi1i 635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
40	39	exbii 1877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
41		breq1 5111	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ 𝑧(V ∖ I )𝑦))
42		brv 5453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧V𝑦
43		brdif 5163	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
44	42, 43	mpbiran 721	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
45	30	ideq 5837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 I 𝑦 ↔ 𝑧 = 𝑦)
46		equcom 2047	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑦 ↔ 𝑦 = 𝑧)
47	45, 46	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 I 𝑦 ↔ 𝑦 = 𝑧)
48	47	notbii 323	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
49	44, 48	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
50	41, 49	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
51	50	equsexvw 2034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
52	37, 40, 51	3bitri 300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
53	36, 52	anbi12i 639	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
54	31, 53	bitri 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
55	28, 54	bitrdi 290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
56	27, 55	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57		an12 657	. . . . . . . . . . . . . . . . 17 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
58	56, 57	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
59	20, 21, 25, 58	ceqsex2v 3505	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
60	19, 59	bitr3i 280	. . . . . . . . . . . . . 14 ⊢ (∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
61	60	exbii 1877	. . . . . . . . . . . . 13 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62		opeq1 4837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
63	62	eleq1d 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
64	63	anbi2d 641	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
65	64	anbi1d 642	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
66	65	equsexvw 2034	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
67	61, 66	bitri 278	. . . . . . . . . . . 12 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
68	67	exbii 1877	. . . . . . . . . . 11 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69		exanali 1888	. . . . . . . . . . 11 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
70	68, 69	bitri 278	. . . . . . . . . 10 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
71	16, 17, 70	3bitri 300	. . . . . . . . 9 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72	71	exbii 1877	. . . . . . . 8 ⊢ (∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73		exnal 1856	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74	15, 72, 73	3bitri 300	. . . . . . 7 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	74	exbii 1877	. . . . . 6 ⊢ (∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76		exnal 1856	. . . . . 6 ⊢ (∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77	14, 75, 76	3bitri 300	. . . . 5 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	13, 77	bitrdi 290	. . . 4 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
79	78	con2bid 357	. . 3 ⊢ (Rel 𝐹 → (∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
80	79	pm5.32i 584	. 2 ⊢ ((Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81		dffun4 6549	. 2 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82		df-funs 36359	. . . 4 ⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
83	82	eleq2i 2854	. . 3 ⊢ (𝐹 ∈ Funs ↔ 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))))
84		eldif 3914	. . 3 ⊢ (𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) ↔ (𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))))
85		elfuns.1	. . . . . 6 ⊢ 𝐹 ∈ V
86	85	elpw 4565	. . . . 5 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87		df-rel 5667	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
88	86, 87	bitr4i 281	. . . 4 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
89	85	elfix 36401	. . . . . 6 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹)
90	85, 85	coep 36252	. . . . . . 7 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝)
91		vex 3458	. . . . . . . . 9 ⊢ 𝑝 ∈ V
92	85, 91	coepr 36253	. . . . . . . 8 ⊢ (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
93	92	rexbii 3111	. . . . . . 7 ⊢ (∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
94	90, 93	bitri 278	. . . . . 6 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95		r2ex 3201	. . . . . 6 ⊢ (∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
96	89, 94, 95	3bitri 300	. . . . 5 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
97	96	notbii 323	. . . 4 ⊢ (¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
98	88, 97	anbi12i 639	. . 3 ⊢ ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
99	83, 84, 98	3bitri 300	. 2 ⊢ (𝐹 ∈ Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
100	80, 81, 99	3bitr4ri 307	1 ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102  ∀wal 1567   = wceq 1569  ∃wex 1808   ∈ wcel 2142  ∃wrex 3088  Vcvv 3454   ∖ cdif 3901   ⊆ wss 3904  𝒫 cpw 4561  ⟨cop 4594   class class class wbr 5108   I cid 5554   E cep 5559   × cxp 5658  ^◡ccnv 5659   ∘ ccom 5664  Rel wrel 5665  Fun wfun 6530  1^st c1st 7982  2^nd c2nd 7983   ⊗ ctxp 36328   Fix cfix 36333   Funs cfuns 36335

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-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  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-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-eprel 5560  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fo 6542  df-fv 6544  df-1st 7984  df-2nd 7985  df-txp 36352  df-fix 36357  df-funs 36359

This theorem is used by:  elfunsg  36414  dfrecs2  36450  dfrdg4  36451