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

Theorem elfuns 35916
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 5808 . . . . . . . . . . 11 ((Rel 𝐹𝑝𝐹) → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
21ex 412 . . . . . . . . . 10 (Rel 𝐹 → (𝑝𝐹 → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3 elrel 5808 . . . . . . . . . . 11 ((Rel 𝐹𝑞𝐹) → ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
43ex 412 . . . . . . . . . 10 (Rel 𝐹 → (𝑞𝐹 → ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
52, 4anim12d 609 . . . . . . . . 9 (Rel 𝐹 → ((𝑝𝐹𝑞𝐹) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
65adantrd 491 . . . . . . . 8 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
76pm4.71rd 562 . . . . . . 7 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8 19.41vvvv 1952 . . . . . . . 8 (∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9 ee4anv 2353 . . . . . . . . 9 (∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
109anbi1i 624 . . . . . . . 8 ((∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
118, 10bitr2i 276 . . . . . . 7 (((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
127, 11bitrdi 287 . . . . . 6 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13122exbidv 1924 . . . . 5 (Rel 𝐹 → (∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14 excom13 2164 . . . . . 6 (∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15 excom13 2164 . . . . . . . 8 (∃𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16 exrot4 2166 . . . . . . . . . 10 (∃𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎𝑧𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17 excom 2162 . . . . . . . . . 10 (∃𝑎𝑧𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18 df-3an 1089 . . . . . . . . . . . . . . . 16 ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19182exbii 1849 . . . . . . . . . . . . . . 15 (∃𝑝𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20 opex 5469 . . . . . . . . . . . . . . . 16 𝑥, 𝑦⟩ ∈ V
21 opex 5469 . . . . . . . . . . . . . . . 16 𝑎, 𝑧⟩ ∈ V
22 eleq1 2829 . . . . . . . . . . . . . . . . . 18 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
2322anbi1d 631 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝𝐹𝑞𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹)))
24 breq2 5147 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
2523, 24anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26 eleq1 2829 . . . . . . . . . . . . . . . . . . 19 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
2726anbi2d 630 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28 breq1 5146 . . . . . . . . . . . . . . . . . . 19 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
30 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
3121, 29, 30brtxp 35881 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32 vex 3484 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
33 vex 3484 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
3432, 33br1steq 35771 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑎, 𝑧⟩1st 𝑥𝑥 = 𝑎)
35 equcom 2017 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎𝑎 = 𝑥)
3634, 35bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑧⟩1st 𝑥𝑎 = 𝑥)
3721, 30brco 5881 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦))
3832, 33br2ndeq 35772 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑧⟩2nd 𝑥𝑥 = 𝑧)
3938anbi1i 624 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧𝑥(V ∖ I )𝑦))
4039exbii 1848 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧𝑥(V ∖ I )𝑦))
41 breq1 5146 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦𝑧(V ∖ I )𝑦))
42 brv 5477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧V𝑦
43 brdif 5196 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
4442, 43mpbiran 709 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
4530ideq 5863 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 I 𝑦𝑧 = 𝑦)
46 equcom 2017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦𝑦 = 𝑧)
4745, 46bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 I 𝑦𝑦 = 𝑧)
4847notbii 320 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
4944, 48bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
5041, 49bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
5150equsexvw 2004 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥(𝑥 = 𝑧𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
5237, 40, 513bitri 297 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
5336, 52anbi12i 628 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
5431, 53bitri 275 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
5528, 54bitrdi 287 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
5627, 55anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57 an12 645 . . . . . . . . . . . . . . . . 17 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
5856, 57bitrdi 287 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
5920, 21, 25, 58ceqsex2v 3536 . . . . . . . . . . . . . . 15 (∃𝑝𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6019, 59bitr3i 277 . . . . . . . . . . . . . 14 (∃𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6160exbii 1848 . . . . . . . . . . . . 13 (∃𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62 opeq1 4873 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
6362eleq1d 2826 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
6463anbi2d 630 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
6564anbi1d 631 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6665equsexvw 2004 . . . . . . . . . . . . 13 (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
6761, 66bitri 275 . . . . . . . . . . . 12 (∃𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
6867exbii 1848 . . . . . . . . . . 11 (∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69 exanali 1859 . . . . . . . . . . 11 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7068, 69bitri 275 . . . . . . . . . 10 (∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7116, 17, 703bitri 297 . . . . . . . . 9 (∃𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7271exbii 1848 . . . . . . . 8 (∃𝑦𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73 exnal 1827 . . . . . . . 8 (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7415, 72, 733bitri 297 . . . . . . 7 (∃𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7574exbii 1848 . . . . . 6 (∃𝑥𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76 exnal 1827 . . . . . 6 (∃𝑥 ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7714, 75, 763bitri 297 . . . . 5 (∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7813, 77bitrdi 287 . . . 4 (Rel 𝐹 → (∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
7978con2bid 354 . . 3 (Rel 𝐹 → (∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
8079pm5.32i 574 . 2 ((Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81 dffun4 6577 . 2 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82 df-funs 35862 . . . 4 Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )))
8382eleq2i 2833 . . 3 (𝐹 Funs 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))))
84 eldif 3961 . . 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 4604 . . . . 5 (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87 df-rel 5692 . . . . 5 (Rel 𝐹𝐹 ⊆ (V × V))
8886, 87bitr4i 278 . . . 4 (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
8985elfix 35904 . . . . . 6 (𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹)
9085, 85coep 35752 . . . . . . 7 (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹 ↔ ∃𝑝𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝)
91 vex 3484 . . . . . . . . 9 𝑝 ∈ V
9285, 91coepr 35753 . . . . . . . 8 (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝 ↔ ∃𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
9392rexbii 3094 . . . . . . 7 (∃𝑝𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝 ↔ ∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
9490, 93bitri 275 . . . . . 6 (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹 ↔ ∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95 r2ex 3196 . . . . . 6 (∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9689, 94, 953bitri 297 . . . . 5 (𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9796notbii 320 . . . 4 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9888, 97anbi12i 628 . . 3 ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9983, 84, 983bitri 297 . 2 (𝐹 Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
10080, 81, 993bitr4ri 304 1 (𝐹 Funs ↔ Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087  wal 1538   = wceq 1540  wex 1779  wcel 2108  wrex 3070  Vcvv 3480  cdif 3948  wss 3951  𝒫 cpw 4600  cop 4632   class class class wbr 5143   I cid 5577   E cep 5583   × cxp 5683  ccnv 5684  ccom 5689  Rel wrel 5690  Fun wfun 6555  1st c1st 8012  2nd c2nd 8013  ctxp 35831   Fix cfix 35836   Funs cfuns 35838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-eprel 5584  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fo 6567  df-fv 6569  df-1st 8014  df-2nd 8015  df-txp 35855  df-fix 35860  df-funs 35862
This theorem is referenced by:  elfunsg  35917  dfrecs2  35951  dfrdg4  35952
  Copyright terms: Public domain W3C validator