Theorem elfuns 32022

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 5222	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑝 ∈ 𝐹) → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
2	1	ex 450	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑝 ∈ 𝐹 → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3		elrel 5222	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑞 ∈ 𝐹) → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
4	3	ex 450	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑞 ∈ 𝐹 → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
5	2, 4	anim12d 586	. . . . . . . . 9 ⊢ (Rel 𝐹 → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
6	5	adantrd 484	. . . . . . . 8 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
7	6	pm4.71rd 667	. . . . . . 7 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8		19.41vvvv 1917	. . . . . . . 8 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9		ee4anv 2184	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
10	9	anbi1i 731	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
11	8, 10	bitr2i 265	. . . . . . 7 ⊢ (((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
12	7, 11	syl6bb 276	. . . . . 6 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13	12	2exbidv 1852	. . . . 5 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14		excom13 2044	. . . . . 6 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15		excom13 2044	. . . . . . . 8 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16		exrot4 2046	. . . . . . . . . 10 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17		excom 2042	. . . . . . . . . 10 ⊢ (∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18		df-3an 1039	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19	18	2exbii 1775	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20		opex 4932	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
21		opex 4932	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑧⟩ ∈ V
22		eleq1 2689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
23	22	anbi1d 741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹)))
24		breq2 4657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
25	23, 24	anbi12d 747	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞 ∈ 𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
27	26	anbi2d 740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28		breq1 4656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
30		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
31	21, 29, 30	brtxp 31987	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32		vex 3203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
33		vex 3203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
34	32, 33	br1steq 31670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑥 = 𝑎)
35		equcom 1945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 ↔ 𝑎 = 𝑥)
36	34, 35	bitri 264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑎 = 𝑥)
37	21, 30	brco 5292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦))
38	32, 33	br2ndeq 31671	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑧⟩2nd 𝑥 ↔ 𝑥 = 𝑧)
39	38	anbi1i 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
40	39	exbii 1774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
41		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ 𝑧(V ∖ I )𝑦))
42		brv 4941	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧V𝑦
43		brdif 4705	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
44	42, 43	mpbiran 953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
45	30	ideq 5274	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 I 𝑦 ↔ 𝑧 = 𝑦)
46		equcom 1945	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑦 ↔ 𝑦 = 𝑧)
47	45, 46	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 I 𝑦 ↔ 𝑦 = 𝑧)
48	47	notbii 310	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
49	44, 48	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
50	41, 49	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
51	50	equsexvw 1932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
52	37, 40, 51	3bitri 286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
53	36, 52	anbi12i 733	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
54	31, 53	bitri 264	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
55	28, 54	syl6bb 276	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
56	27, 55	anbi12d 747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57		an12 838	. . . . . . . . . . . . . . . . 17 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
58	56, 57	syl6bb 276	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
59	20, 21, 25, 58	ceqsex2v 3245	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
60	19, 59	bitr3i 266	. . . . . . . . . . . . . 14 ⊢ (∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
61	60	exbii 1774	. . . . . . . . . . . . 13 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62		opeq1 4402	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
63	62	eleq1d 2686	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
64	63	anbi2d 740	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
65	64	anbi1d 741	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
66	65	equsexvw 1932	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
67	61, 66	bitri 264	. . . . . . . . . . . 12 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
68	67	exbii 1774	. . . . . . . . . . 11 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69		exanali 1786	. . . . . . . . . . 11 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
70	68, 69	bitri 264	. . . . . . . . . 10 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
71	16, 17, 70	3bitri 286	. . . . . . . . 9 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72	71	exbii 1774	. . . . . . . 8 ⊢ (∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73		exnal 1754	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74	15, 72, 73	3bitri 286	. . . . . . 7 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	74	exbii 1774	. . . . . 6 ⊢ (∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76		exnal 1754	. . . . . 6 ⊢ (∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77	14, 75, 76	3bitri 286	. . . . 5 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	13, 77	syl6bb 276	. . . 4 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
79	78	con2bid 344	. . 3 ⊢ (Rel 𝐹 → (∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
80	79	pm5.32i 669	. 2 ⊢ ((Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81		dffun4 5900	. 2 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82		df-funs 31968	. . . 4 ⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
83	82	eleq2i 2693	. . 3 ⊢ (𝐹 ∈ Funs ↔ 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))))
84		eldif 3584	. . 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 4164	. . . . 5 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87		df-rel 5121	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
88	86, 87	bitr4i 267	. . . 4 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
89	85	elfix 32010	. . . . . 6 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹)
90	85, 85	coep 31641	. . . . . . 7 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝)
91		vex 3203	. . . . . . . . 9 ⊢ 𝑝 ∈ V
92	85, 91	coepr 31642	. . . . . . . 8 ⊢ (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
93	92	rexbii 3041	. . . . . . 7 ⊢ (∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
94	90, 93	bitri 264	. . . . . 6 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95		r2ex 3061	. . . . . 6 ⊢ (∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
96	89, 94, 95	3bitri 286	. . . . 5 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
97	96	notbii 310	. . . 4 ⊢ (¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
98	88, 97	anbi12i 733	. . 3 ⊢ ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
99	83, 84, 98	3bitri 286	. 2 ⊢ (𝐹 ∈ Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
100	80, 81, 99	3bitr4ri 293	1 ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913  Vcvv 3200   ∖ cdif 3571   ⊆ wss 3574  𝒫 cpw 4158  ⟨cop 4183   class class class wbr 4653   I cid 5023   E cep 5028   × cxp 5112  ^◡ccnv 5113   ∘ ccom 5118  Rel wrel 5119  Fun wfun 5882  1^st c1st 7166  2^nd c2nd 7167   ⊗ ctxp 31937   Fix cfix 31942   Funs cfuns 31944

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-eprel 5029  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fo 5894  df-fv 5896  df-1st 7168  df-2nd 7169  df-txp 31961  df-fix 31966  df-funs 31968

This theorem is referenced by:  elfunsg  32023  dfrecs2  32057  dfrdg4  32058