Theorem elfuns 36268

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 5772	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑝 ∈ 𝐹) → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
2	1	ex 416	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑝 ∈ 𝐹 → ∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3		elrel 5772	. . . . . . . . . . 11 ⊢ ((Rel 𝐹 ∧ 𝑞 ∈ 𝐹) → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
4	3	ex 416	. . . . . . . . . 10 ⊢ (Rel 𝐹 → (𝑞 ∈ 𝐹 → ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
5	2, 4	anim12d 618	. . . . . . . . 9 ⊢ (Rel 𝐹 → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
6	5	adantrd 495	. . . . . . . 8 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
7	6	pm4.71rd 570	. . . . . . 7 ⊢ (Rel 𝐹 → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8		19.41vvvv 1974	. . . . . . . 8 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9		ee4anv 2384	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦∃𝑎∃𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥∃𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎∃𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
10	9	anbi1i 633	. . . . . . . 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 1946	. . . . 5 ⊢ (Rel 𝐹 → (∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14		excom13 2200	. . . . . 6 ⊢ (∃𝑝∃𝑞∃𝑥∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15		excom13 2200	. . . . . . . 8 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16		exrot4 2202	. . . . . . . . . 10 ⊢ (∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17		excom 2198	. . . . . . . . . 10 ⊢ (∃𝑎∃𝑧∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18		df-3an 1101	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19	18	2exbii 1871	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20		opex 5433	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
21		opex 5433	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑧⟩ ∈ V
22		eleq1 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
23	22	anbi1d 640	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹)))
24		breq2 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
25	23, 24	anbi12d 641	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26		eleq1 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞 ∈ 𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
27	26	anbi2d 639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28		breq1 5105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29		vex 3460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
30		vex 3460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
31	21, 29, 30	brtxp 36233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32		vex 3460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
33		vex 3460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
34	32, 33	br1steq 36126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑥 = 𝑎)
35		equcom 2040	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 ↔ 𝑎 = 𝑥)
36	34, 35	bitri 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩1st 𝑥 ↔ 𝑎 = 𝑥)
37	21, 30	brco 5844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦))
38	32, 33	br2ndeq 36127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑧⟩2nd 𝑥 ↔ 𝑥 = 𝑧)
39	38	anbi1i 633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
40	39	exbii 1870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥 ∧ 𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦))
41		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ 𝑧(V ∖ I )𝑦))
42		brv 5442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧V𝑦
43		brdif 5155	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
44	42, 43	mpbiran 719	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
45	30	ideq 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 I 𝑦 ↔ 𝑧 = 𝑦)
46		equcom 2040	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2027	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥(𝑥 = 𝑧 ∧ 𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
52	37, 40, 51	3bitri 299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
53	36, 52	anbi12i 637	. . . . . . . . . . . . . . . . . . . 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 641	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57		an12 655	. . . . . . . . . . . . . . . . 17 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
58	56, 57	bitrdi 289	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
59	20, 21, 25, 58	ceqsex2v 3507	. . . . . . . . . . . . . . 15 ⊢ (∃𝑝∃𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
60	19, 59	bitr3i 279	. . . . . . . . . . . . . 14 ⊢ (∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
61	60	exbii 1870	. . . . . . . . . . . . 13 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62		opeq1 4833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
63	62	eleq1d 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
64	63	anbi2d 639	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
65	64	anbi1d 640	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
66	65	equsexvw 2027	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
67	61, 66	bitri 277	. . . . . . . . . . . 12 ⊢ (∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
68	67	exbii 1870	. . . . . . . . . . 11 ⊢ (∃𝑧∃𝑎∃𝑝∃𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69		exanali 1881	. . . . . . . . . . 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 1870	. . . . . . . 8 ⊢ (∃𝑦∃𝑝∃𝑞∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73		exnal 1849	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74	15, 72, 73	3bitri 299	. . . . . . 7 ⊢ (∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	74	exbii 1870	. . . . . 6 ⊢ (∃𝑥∃𝑞∃𝑝∃𝑦∃𝑎∃𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76		exnal 1849	. . . . . 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 582	. 2 ⊢ ((Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝∃𝑞((𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81		dffun4 6536	. 2 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82		df-funs 36214	. . . 4 ⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
83	82	eleq2i 2856	. . 3 ⊢ (𝐹 ∈ Funs ↔ 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))))
84		eldif 3916	. . 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 4561	. . . . 5 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87		df-rel 5656	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
88	86, 87	bitr4i 280	. . . 4 ⊢ (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
89	85	elfix 36256	. . . . . 6 ⊢ (𝐹 ∈ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹)
90	85, 85	coep 36107	. . . . . . 7 ⊢ (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))𝐹 ↔ ∃𝑝 ∈ 𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )𝑝)
91		vex 3460	. . . . . . . . 9 ⊢ 𝑝 ∈ V
92	85, 91	coepr 36108	. . . . . . . 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 277	. . . . . 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 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 637	. . 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 399   ∧ w3a 1099  ∀wal 1560   = wceq 1562  ∃wex 1801   ∈ wcel 2144  ∃wrex 3088  Vcvv 3456   ∖ cdif 3903   ⊆ wss 3906  𝒫 cpw 4557  ⟨cop 4590   class class class wbr 5102   I cid 5543   E cep 5548   × cxp 5647  ^◡ccnv 5648   ∘ ccom 5653  Rel wrel 5654  Fun wfun 6517  1^st c1st 7970  2^nd c2nd 7971   ⊗ ctxp 36183   Fix cfix 36188   Funs cfuns 36190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-eprel 5549  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-fo 6529  df-fv 6531  df-1st 7972  df-2nd 7973  df-txp 36207  df-fix 36212  df-funs 36214

This theorem is referenced by:  elfunsg  36269  dfrecs2  36305  dfrdg4  36306