Theorem elfuns 32837

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 5514	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑝 ∈ 𝐹) → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
2	1	ex 405	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑝 ∈ 𝐹 → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3		elrel 5514	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑞 ∈ 𝐹) → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
4	3	ex 405	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑞 ∈ 𝐹 → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
5	2, 4	anim12d 599	. . . . . . . . 9 ⊢ (Rel 𝐹 → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
6	5	adantrd 484	. . . . . . . 8 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
7	6	pm4.71rd 555	. . . . . . 7 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8		19.41vvvv 1911	. . . . . . . 8 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9		ee4anv 2283	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
10	9	anbi1i 614	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
11	8, 10	bitr2i 268	. . . . . . 7 ⊢ (((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
12	7, 11	syl6bb 279	. . . . . 6 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13	12	2exbidv 1883	. . . . 5 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14		excom13 2098	. . . . . 6 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15		excom13 2098	. . . . . . . 8 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16		exrot4 2100	. . . . . . . . . 10 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17		excom 2096	. . . . . . . . . 10 ⊢ (∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18		df-3an 1070	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19	18	2exbii 1811	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20		opex 5206	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
21		opex 5206	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑧⟩ ∈ V
22		eleq1 2847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
23	22	anbi1d 620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹)))
24		breq2 4927	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
25	23, 24	anbi12d 621	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26		eleq1 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞 ∈ 𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
27	26	anbi2d 619	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28		breq1 4926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29		vex 3412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
30		vex 3412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
31	21, 29, 30	brtxp 32802	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32		vex 3412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
33		vex 3412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
34	32, 33	br1steq 32474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑥 = 𝑎)
35		equcom 1974	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 ↔ 𝑎 = 𝑥)
36	34, 35	bitri 267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑎 = 𝑥)
37	21, 30	brco 5584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦))
38	32, 33	br2ndeq 32475	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑧⟩2nd 𝑥 ↔ 𝑥 = 𝑧)
39	38	anbi1i 614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
40	39	exbii 1810	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
41		breq1 4926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ 𝑧(V ∖ I )𝑦))
42		brv 5214	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧V𝑦
43		brdif 4976	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
44	42, 43	mpbiran 696	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
45	30	ideq 5566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 I 𝑦 ↔ 𝑧 = 𝑦)
46		equcom 1974	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑦 ↔ 𝑦 = 𝑧)
47	45, 46	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 I 𝑦 ↔ 𝑦 = 𝑧)
48	47	notbii 312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
49	44, 48	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
50	41, 49	syl6bb 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
51	50	equsexvw 1961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
52	37, 40, 51	3bitri 289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
53	36, 52	anbi12i 617	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
54	31, 53	bitri 267	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
55	28, 54	syl6bb 279	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
56	27, 55	anbi12d 621	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57		an12 632	. . . . . . . . . . . . . . . . 17 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
58	56, 57	syl6bb 279	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
59	20, 21, 25, 58	ceqsex2v 3459	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
60	19, 59	bitr3i 269	. . . . . . . . . . . . . 14 ⊢ (∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
61	60	exbii 1810	. . . . . . . . . . . . 13 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62		opeq1 4671	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
63	62	eleq1d 2844	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
64	63	anbi2d 619	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
65	64	anbi1d 620	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
66	65	equsexvw 1961	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
67	61, 66	bitri 267	. . . . . . . . . . . 12 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
68	67	exbii 1810	. . . . . . . . . . 11 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69		exanali 1821	. . . . . . . . . . 11 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
70	68, 69	bitri 267	. . . . . . . . . 10 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
71	16, 17, 70	3bitri 289	. . . . . . . . 9 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72	71	exbii 1810	. . . . . . . 8 ⊢ (∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73		exnal 1789	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74	15, 72, 73	3bitri 289	. . . . . . 7 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	74	exbii 1810	. . . . . 6 ⊢ (∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76		exnal 1789	. . . . . 6 ⊢ (∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77	14, 75, 76	3bitri 289	. . . . 5 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	13, 77	syl6bb 279	. . . 4 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
79	78	con2bid 347	. . 3 ⊢ (Rel 𝐹 → (∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
80	79	pm5.32i 567	. 2 ⊢ ((Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81		dffun4 6194	. 2 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82		df-funs 32783	. . . 4 ⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
83	82	eleq2i 2851	. . 3 ⊢ (𝐹 ∈ Funs ↔ 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))))
84		eldif 3835	. . 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 4422	. . . . 5 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87		df-rel 5407	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
88	86, 87	bitr4i 270	. . . 4 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
89	85	elfix 32825	. . . . . 6 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹)
90	85, 85	coep 32447	. . . . . . 7 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝)
91		vex 3412	. . . . . . . . 9 ⊢ 𝑝 ∈ V
92	85, 91	coepr 32448	. . . . . . . 8 ⊢ (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
93	92	rexbii 3188	. . . . . . 7 ⊢ (∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
94	90, 93	bitri 267	. . . . . 6 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95		r2ex 3242	. . . . . 6 ⊢ (∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
96	89, 94, 95	3bitri 289	. . . . 5 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
97	96	notbii 312	. . . 4 ⊢ (¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
98	88, 97	anbi12i 617	. . 3 ⊢ ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
99	83, 84, 98	3bitri 289	. 2 ⊢ (𝐹 ∈ Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
100	80, 81, 99	3bitr4ri 296	1 ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068  ∀wal 1505   = wceq 1507  ∃wex 1742   ∈ wcel 2048  ∃wrex 3083  Vcvv 3409   ∖ cdif 3822   ⊆ wss 3825  𝒫 cpw 4416  ⟨cop 4441   class class class wbr 4923   I cid 5304   E cep 5309   × cxp 5398  ^◡ccnv 5399   ∘ ccom 5404  Rel wrel 5405  Fun wfun 6176  1^st c1st 7492  2^nd c2nd 7493   ⊗ ctxp 32752   Fix cfix 32757   Funs cfuns 32759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-eprel 5310  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-fo 6188  df-fv 6190  df-1st 7494  df-2nd 7495  df-txp 32776  df-fix 32781  df-funs 32783

This theorem is referenced by:  elfunsg  32838  dfrecs2  32872  dfrdg4  32873