Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elfuns Structured version   Visualization version   GIF version

Theorem elfuns 32328
 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.
StepHypRef Expression
1 elrel 5379 . . . . . . . . . . 11 ((Rel 𝐹𝑝𝐹) → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
21ex 449 . . . . . . . . . 10 (Rel 𝐹 → (𝑝𝐹 → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3 elrel 5379 . . . . . . . . . . 11 ((Rel 𝐹𝑞𝐹) → ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
43ex 449 . . . . . . . . . 10 (Rel 𝐹 → (𝑞𝐹 → ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
52, 4anim12d 587 . . . . . . . . 9 (Rel 𝐹 → ((𝑝𝐹𝑞𝐹) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
65adantrd 485 . . . . . . . 8 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
76pm4.71rd 670 . . . . . . 7 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8 19.41vvvv 2029 . . . . . . . 8 (∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9 ee4anv 2329 . . . . . . . . 9 (∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
109anbi1i 733 . . . . . . . 8 ((∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
118, 10bitr2i 265 . . . . . . 7 (((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
127, 11syl6bb 276 . . . . . 6 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13122exbidv 2001 . . . . 5 (Rel 𝐹 → (∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14 excom13 2193 . . . . . 6 (∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15 excom13 2193 . . . . . . . 8 (∃𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16 exrot4 2195 . . . . . . . . . 10 (∃𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎𝑧𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17 excom 2191 . . . . . . . . . 10 (∃𝑎𝑧𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18 df-3an 1074 . . . . . . . . . . . . . . . 16 ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19182exbii 1924 . . . . . . . . . . . . . . 15 (∃𝑝𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20 opex 5081 . . . . . . . . . . . . . . . 16 𝑥, 𝑦⟩ ∈ V
21 opex 5081 . . . . . . . . . . . . . . . 16 𝑎, 𝑧⟩ ∈ V
22 eleq1 2827 . . . . . . . . . . . . . . . . . 18 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
2322anbi1d 743 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝𝐹𝑞𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹)))
24 breq2 4808 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
2523, 24anbi12d 749 . . . . . . . . . . . . . . . 16 (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26 eleq1 2827 . . . . . . . . . . . . . . . . . . 19 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
2726anbi2d 742 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28 breq1 4807 . . . . . . . . . . . . . . . . . . 19 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29 vex 3343 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
30 vex 3343 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
3121, 29, 30brtxp 32293 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32 vex 3343 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
33 vex 3343 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
3432, 33br1steq 31977 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑎, 𝑧⟩1st 𝑥𝑥 = 𝑎)
35 equcom 2100 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎𝑎 = 𝑥)
3634, 35bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑧⟩1st 𝑥𝑎 = 𝑥)
3721, 30brco 5448 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦))
3832, 33br2ndeq 31978 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑧⟩2nd 𝑥𝑥 = 𝑧)
3938anbi1i 733 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧𝑥(V ∖ I )𝑦))
4039exbii 1923 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧𝑥(V ∖ I )𝑦))
41 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦𝑧(V ∖ I )𝑦))
42 brv 5089 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧V𝑦
43 brdif 4857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
4442, 43mpbiran 991 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
4530ideq 5430 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 I 𝑦𝑧 = 𝑦)
46 equcom 2100 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦𝑦 = 𝑧)
4745, 46bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 I 𝑦𝑦 = 𝑧)
4847notbii 309 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
4944, 48bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
5041, 49syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
5150equsexvw 2087 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥(𝑥 = 𝑧𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
5237, 40, 513bitri 286 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
5336, 52anbi12i 735 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
5431, 53bitri 264 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
5528, 54syl6bb 276 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
5627, 55anbi12d 749 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57 an12 873 . . . . . . . . . . . . . . . . 17 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
5856, 57syl6bb 276 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
5920, 21, 25, 58ceqsex2v 3385 . . . . . . . . . . . . . . 15 (∃𝑝𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6019, 59bitr3i 266 . . . . . . . . . . . . . 14 (∃𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6160exbii 1923 . . . . . . . . . . . . 13 (∃𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62 opeq1 4553 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
6362eleq1d 2824 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
6463anbi2d 742 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
6564anbi1d 743 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6665equsexvw 2087 . . . . . . . . . . . . 13 (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
6761, 66bitri 264 . . . . . . . . . . . 12 (∃𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
6867exbii 1923 . . . . . . . . . . 11 (∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69 exanali 1935 . . . . . . . . . . 11 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7068, 69bitri 264 . . . . . . . . . 10 (∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7116, 17, 703bitri 286 . . . . . . . . 9 (∃𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7271exbii 1923 . . . . . . . 8 (∃𝑦𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73 exnal 1903 . . . . . . . 8 (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7415, 72, 733bitri 286 . . . . . . 7 (∃𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7574exbii 1923 . . . . . 6 (∃𝑥𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76 exnal 1903 . . . . . 6 (∃𝑥 ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7714, 75, 763bitri 286 . . . . 5 (∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7813, 77syl6bb 276 . . . 4 (Rel 𝐹 → (∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
7978con2bid 343 . . 3 (Rel 𝐹 → (∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
8079pm5.32i 672 . 2 ((Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81 dffun4 6061 . 2 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82 df-funs 32274 . . . 4 Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )))
8382eleq2i 2831 . . 3 (𝐹 Funs 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))))
84 eldif 3725 . . 3 (𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))) ↔ (𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))))
85 elfuns.1 . . . . . 6 𝐹 ∈ V
8685elpw 4308 . . . . 5 (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87 df-rel 5273 . . . . 5 (Rel 𝐹𝐹 ⊆ (V × V))
8886, 87bitr4i 267 . . . 4 (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
8985elfix 32316 . . . . . 6 (𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹)
9085, 85coep 31948 . . . . . . 7 (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹 ↔ ∃𝑝𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝)
91 vex 3343 . . . . . . . . 9 𝑝 ∈ V
9285, 91coepr 31949 . . . . . . . 8 (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝 ↔ ∃𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
9392rexbii 3179 . . . . . . 7 (∃𝑝𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝 ↔ ∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
9490, 93bitri 264 . . . . . 6 (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹 ↔ ∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95 r2ex 3199 . . . . . 6 (∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9689, 94, 953bitri 286 . . . . 5 (𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9796notbii 309 . . . 4 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9888, 97anbi12i 735 . . 3 ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9983, 84, 983bitri 286 . 2 (𝐹 Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
10080, 81, 993bitr4ri 293 1 (𝐹 Funs ↔ Fun 𝐹)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072  ∀wal 1630   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∃wrex 3051  Vcvv 3340   ∖ cdif 3712   ⊆ wss 3715  𝒫 cpw 4302  ⟨cop 4327   class class class wbr 4804   I cid 5173   E cep 5178   × cxp 5264  ◡ccnv 5265   ∘ ccom 5270  Rel wrel 5271  Fun wfun 6043  1st c1st 7331  2nd c2nd 7332   ⊗ ctxp 32243   Fix cfix 32248   Funs cfuns 32250 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-eprel 5179  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fo 6055  df-fv 6057  df-1st 7333  df-2nd 7334  df-txp 32267  df-fix 32272  df-funs 32274 This theorem is referenced by:  elfunsg  32329  dfrecs2  32363  dfrdg4  32364
 Copyright terms: Public domain W3C validator