Theorem elfuns 36156

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 5744	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑝 ∈ 𝐹) → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
2	1	ex 414	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑝 ∈ 𝐹 → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3		elrel 5744	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑞 ∈ 𝐹) → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
4	3	ex 414	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑞 ∈ 𝐹 → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
5	2, 4	anim12d 616	. . . . . . . . 9 ⊢ (Rel 𝐹 → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
6	5	adantrd 493	. . . . . . . 8 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
7	6	pm4.71rd 568	. . . . . . 7 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8		19.41vvvv 1960	. . . . . . . 8 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9		ee4anv 2361	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
10	9	anbi1i 631	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
11	8, 10	bitr2i 278	. . . . . . 7 ⊢ (((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
12	7, 11	bitrdi 289	. . . . . 6 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13	12	2exbidv 1932	. . . . 5 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14		excom13 2177	. . . . . 6 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15		excom13 2177	. . . . . . . 8 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16		exrot4 2179	. . . . . . . . . 10 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17		excom 2175	. . . . . . . . . 10 ⊢ (∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18		df-3an 1095	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19	18	2exbii 1857	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20		opex 5406	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
21		opex 5406	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑧⟩ ∈ V
22		eleq1 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
23	22	anbi1d 638	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹)))
24		breq2 5079	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
25	23, 24	anbi12d 639	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26		eleq1 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞 ∈ 𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
27	26	anbi2d 637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28		breq1 5078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29		vex 3437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
30		vex 3437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
31	21, 29, 30	brtxp 36121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32		vex 3437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
33		vex 3437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
34	32, 33	br1steq 36014	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑥 = 𝑎)
35		equcom 2026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 ↔ 𝑎 = 𝑥)
36	34, 35	bitri 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑎 = 𝑥)
37	21, 30	brco 5815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦))
38	32, 33	br2ndeq 36015	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑧⟩2nd 𝑥 ↔ 𝑥 = 𝑧)
39	38	anbi1i 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
40	39	exbii 1856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
41		breq1 5078	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ 𝑧(V ∖ I )𝑦))
42		brv 5415	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧V𝑦
43		brdif 5128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
44	42, 43	mpbiran 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
45	30	ideq 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 I 𝑦 ↔ 𝑧 = 𝑦)
46		equcom 2026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑦 ↔ 𝑦 = 𝑧)
47	45, 46	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 I 𝑦 ↔ 𝑦 = 𝑧)
48	47	notbii 322	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
49	44, 48	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
50	41, 49	bitrdi 289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
51	50	equsexvw 2013	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
52	37, 40, 51	3bitri 299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
53	36, 52	anbi12i 635	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
54	31, 53	bitri 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
55	28, 54	bitrdi 289	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
56	27, 55	anbi12d 639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57		an12 652	. . . . . . . . . . . . . . . . 17 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
58	56, 57	bitrdi 289	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
59	20, 21, 25, 58	ceqsex2v 3485	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
60	19, 59	bitr3i 279	. . . . . . . . . . . . . 14 ⊢ (∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
61	60	exbii 1856	. . . . . . . . . . . . 13 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62		opeq1 4807	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
63	62	eleq1d 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
64	63	anbi2d 637	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
65	64	anbi1d 638	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
66	65	equsexvw 2013	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
67	61, 66	bitri 277	. . . . . . . . . . . 12 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
68	67	exbii 1856	. . . . . . . . . . 11 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69		exanali 1867	. . . . . . . . . . 11 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
70	68, 69	bitri 277	. . . . . . . . . 10 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
71	16, 17, 70	3bitri 299	. . . . . . . . 9 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72	71	exbii 1856	. . . . . . . 8 ⊢ (∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73		exnal 1835	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74	15, 72, 73	3bitri 299	. . . . . . 7 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	74	exbii 1856	. . . . . 6 ⊢ (∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76		exnal 1835	. . . . . 6 ⊢ (∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77	14, 75, 76	3bitri 299	. . . . 5 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	13, 77	bitrdi 289	. . . 4 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
79	78	con2bid 356	. . 3 ⊢ (Rel 𝐹 → (∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
80	79	pm5.32i 580	. 2 ⊢ ((Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81		dffun4 6502	. 2 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82		df-funs 36102	. . . 4 ⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
83	82	eleq2i 2833	. . 3 ⊢ (𝐹 ∈ Funs ↔ 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))))
84		eldif 3895	. . 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 4536	. . . . 5 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87		df-rel 5628	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
88	86, 87	bitr4i 280	. . . 4 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
89	85	elfix 36144	. . . . . 6 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹)
90	85, 85	coep 35995	. . . . . . 7 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝)
91		vex 3437	. . . . . . . . 9 ⊢ 𝑝 ∈ V
92	85, 91	coepr 35996	. . . . . . . 8 ⊢ (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
93	92	rexbii 3088	. . . . . . 7 ⊢ (∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
94	90, 93	bitri 277	. . . . . 6 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95		r2ex 3178	. . . . . 6 ⊢ (∃𝑝 ∈ 𝐹 ∃𝑞 ∈ 𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
96	89, 94, 95	3bitri 299	. . . . 5 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
97	96	notbii 322	. . . 4 ⊢ (¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
98	88, 97	anbi12i 635	. . 3 ⊢ ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
99	83, 84, 98	3bitri 299	. 2 ⊢ (𝐹 ∈ Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
100	80, 81, 99	3bitr4ri 306	1 ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397   ∧ w3a 1093  ∀wal 1546   = wceq 1548  ∃wex 1787   ∈ wcel 2121  ∃wrex 3065  Vcvv 3433   ∖ cdif 3882   ⊆ wss 3885  𝒫 cpw 4532  ⟨cop 4564   class class class wbr 5075   I cid 5515   E cep 5520   × cxp 5619  ^◡ccnv 5620   ∘ ccom 5625  Rel wrel 5626  Fun wfun 6483  1^st c1st 7933  2^nd c2nd 7934   ⊗ ctxp 36071   Fix cfix 36076   Funs cfuns 36078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-eprel 5521  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fo 6495  df-fv 6497  df-1st 7935  df-2nd 7936  df-txp 36095  df-fix 36100  df-funs 36102

This theorem is referenced by:  elfunsg  36157  dfrecs2  36193  dfrdg4  36194