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 33954
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 5668 . . . . . . . . . . 11 ((Rel 𝐹𝑝𝐹) → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
21ex 416 . . . . . . . . . 10 (Rel 𝐹 → (𝑝𝐹 → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩))
3 elrel 5668 . . . . . . . . . . 11 ((Rel 𝐹𝑞𝐹) → ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)
43ex 416 . . . . . . . . . 10 (Rel 𝐹 → (𝑞𝐹 → ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
52, 4anim12d 612 . . . . . . . . 9 (Rel 𝐹 → ((𝑝𝐹𝑞𝐹) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
65adantrd 495 . . . . . . . 8 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩)))
76pm4.71rd 566 . . . . . . 7 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
8 19.41vvvv 1961 . . . . . . . 8 (∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9 ee4anv 2352 . . . . . . . . 9 (∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ↔ (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩))
109anbi1i 627 . . . . . . . 8 ((∃𝑥𝑦𝑎𝑧(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
118, 10bitr2i 279 . . . . . . 7 (((∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑎𝑧 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
127, 11bitrdi 290 . . . . . 6 (Rel 𝐹 → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
13122exbidv 1932 . . . . 5 (Rel 𝐹 → (∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))))
14 excom13 2168 . . . . . 6 (∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
15 excom13 2168 . . . . . . . 8 (∃𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
16 exrot4 2170 . . . . . . . . . 10 (∃𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎𝑧𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
17 excom 2166 . . . . . . . . . 10 (∃𝑎𝑧𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
18 df-3an 1091 . . . . . . . . . . . . . . . 16 ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
19182exbii 1856 . . . . . . . . . . . . . . 15 (∃𝑝𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
20 opex 5348 . . . . . . . . . . . . . . . 16 𝑥, 𝑦⟩ ∈ V
21 opex 5348 . . . . . . . . . . . . . . . 16 𝑎, 𝑧⟩ ∈ V
22 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
2322anbi1d 633 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝𝐹𝑞𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹)))
24 breq2 5057 . . . . . . . . . . . . . . . . 17 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
2523, 24anbi12d 634 . . . . . . . . . . . . . . . 16 (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩)))
26 eleq1 2825 . . . . . . . . . . . . . . . . . . 19 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞𝐹 ↔ ⟨𝑎, 𝑧⟩ ∈ 𝐹))
2726anbi2d 632 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑎, 𝑧⟩ → ((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹)))
28 breq1 5056 . . . . . . . . . . . . . . . . . . 19 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩))
29 vex 3412 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
30 vex 3412 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
3121, 29, 30brtxp 33919 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦))
32 vex 3412 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
33 vex 3412 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
3432, 33br1steq 33464 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑎, 𝑧⟩1st 𝑥𝑥 = 𝑎)
35 equcom 2026 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎𝑎 = 𝑥)
3634, 35bitri 278 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑧⟩1st 𝑥𝑎 = 𝑥)
3721, 30brco 5739 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦))
3832, 33br2ndeq 33465 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑎, 𝑧⟩2nd 𝑥𝑥 = 𝑧)
3938anbi1i 627 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦) ↔ (𝑥 = 𝑧𝑥(V ∖ I )𝑦))
4039exbii 1855 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥(⟨𝑎, 𝑧⟩2nd 𝑥𝑥(V ∖ I )𝑦) ↔ ∃𝑥(𝑥 = 𝑧𝑥(V ∖ I )𝑦))
41 breq1 5056 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦𝑧(V ∖ I )𝑦))
42 brv 5356 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧V𝑦
43 brdif 5106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(V ∖ I )𝑦 ↔ (𝑧V𝑦 ∧ ¬ 𝑧 I 𝑦))
4442, 43mpbiran 709 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑧 I 𝑦)
4530ideq 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 I 𝑦𝑧 = 𝑦)
46 equcom 2026 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦𝑦 = 𝑧)
4745, 46bitri 278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 I 𝑦𝑦 = 𝑧)
4847notbii 323 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧)
4944, 48bitri 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧)
5041, 49bitrdi 290 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥(V ∖ I )𝑦 ↔ ¬ 𝑦 = 𝑧))
5150equsexvw 2013 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥(𝑥 = 𝑧𝑥(V ∖ I )𝑦) ↔ ¬ 𝑦 = 𝑧)
5237, 40, 513bitri 300 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦 ↔ ¬ 𝑦 = 𝑧)
5336, 52anbi12i 630 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑧⟩1st 𝑥 ∧ ⟨𝑎, 𝑧⟩((V ∖ I ) ∘ 2nd )𝑦) ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
5431, 53bitri 278 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑧⟩(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))
5528, 54bitrdi 290 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑎, 𝑧⟩ → (𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩ ↔ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)))
5627, 55anbi12d 634 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧))))
57 an12 645 . . . . . . . . . . . . . . . . 17 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ (𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
5856, 57bitrdi 290 . . . . . . . . . . . . . . . 16 (𝑞 = ⟨𝑎, 𝑧⟩ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))⟨𝑥, 𝑦⟩) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))))
5920, 21, 25, 58ceqsex2v 3459 . . . . . . . . . . . . . . 15 (∃𝑝𝑞(𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩ ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6019, 59bitr3i 280 . . . . . . . . . . . . . 14 (∃𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ (𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6160exbii 1855 . . . . . . . . . . . . 13 (∃𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
62 opeq1 4784 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑥 → ⟨𝑎, 𝑧⟩ = ⟨𝑥, 𝑧⟩)
6362eleq1d 2822 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (⟨𝑎, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
6463anbi2d 632 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
6564anbi1d 633 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)))
6665equsexvw 2013 . . . . . . . . . . . . 13 (∃𝑎(𝑎 = 𝑥 ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑎, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
6761, 66bitri 278 . . . . . . . . . . . 12 (∃𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
6867exbii 1855 . . . . . . . . . . 11 (∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
69 exanali 1867 . . . . . . . . . . 11 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7068, 69bitri 278 . . . . . . . . . 10 (∃𝑧𝑎𝑝𝑞((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7116, 17, 703bitri 300 . . . . . . . . 9 (∃𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7271exbii 1855 . . . . . . . 8 (∃𝑦𝑝𝑞𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
73 exnal 1834 . . . . . . . 8 (∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7415, 72, 733bitri 300 . . . . . . 7 (∃𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7574exbii 1855 . . . . . 6 (∃𝑥𝑞𝑝𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ∃𝑥 ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76 exnal 1834 . . . . . 6 (∃𝑥 ¬ ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7714, 75, 763bitri 300 . . . . 5 (∃𝑝𝑞𝑥𝑦𝑎𝑧((𝑝 = ⟨𝑥, 𝑦⟩ ∧ 𝑞 = ⟨𝑎, 𝑧⟩) ∧ ((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7813, 77bitrdi 290 . . . 4 (Rel 𝐹 → (∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝) ↔ ¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
7978con2bid 358 . . 3 (Rel 𝐹 → (∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
8079pm5.32i 578 . 2 ((Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
81 dffun4 6392 . 2 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
82 df-funs 33900 . . . 4 Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )))
8382eleq2i 2829 . . 3 (𝐹 Funs 𝐹 ∈ (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))))
84 eldif 3876 . . 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 4517 . . . . 5 (𝐹 ∈ 𝒫 (V × V) ↔ 𝐹 ⊆ (V × V))
87 df-rel 5558 . . . . 5 (Rel 𝐹𝐹 ⊆ (V × V))
8886, 87bitr4i 281 . . . 4 (𝐹 ∈ 𝒫 (V × V) ↔ Rel 𝐹)
8985elfix 33942 . . . . . 6 (𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ 𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹)
9085, 85coep 33437 . . . . . . 7 (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹 ↔ ∃𝑝𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝)
91 vex 3412 . . . . . . . . 9 𝑝 ∈ V
9285, 91coepr 33438 . . . . . . . 8 (𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝 ↔ ∃𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
9392rexbii 3170 . . . . . . 7 (∃𝑝𝐹 𝐹((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )𝑝 ↔ ∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
9490, 93bitri 278 . . . . . 6 (𝐹( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))𝐹 ↔ ∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)
95 r2ex 3222 . . . . . 6 (∃𝑝𝐹𝑞𝐹 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝 ↔ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9689, 94, 953bitri 300 . . . . 5 (𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9796notbii 323 . . . 4 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )) ↔ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝))
9888, 97anbi12i 630 . . 3 ((𝐹 ∈ 𝒫 (V × V) ∧ ¬ 𝐹 Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))) ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
9983, 84, 983bitri 300 . 2 (𝐹 Funs ↔ (Rel 𝐹 ∧ ¬ ∃𝑝𝑞((𝑝𝐹𝑞𝐹) ∧ 𝑞(1st ⊗ ((V ∖ I ) ∘ 2nd ))𝑝)))
10080, 81, 993bitr4ri 307 1 (𝐹 Funs ↔ Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1089  wal 1541   = wceq 1543  wex 1787  wcel 2110  wrex 3062  Vcvv 3408  cdif 3863  wss 3866  𝒫 cpw 4513  cop 4547   class class class wbr 5053   I cid 5454   E cep 5459   × cxp 5549  ccnv 5550  ccom 5555  Rel wrel 5556  Fun wfun 6374  1st c1st 7759  2nd c2nd 7760  ctxp 33869   Fix cfix 33874   Funs cfuns 33876
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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-eprel 5460  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fo 6386  df-fv 6388  df-1st 7761  df-2nd 7762  df-txp 33893  df-fix 33898  df-funs 33900
This theorem is referenced by:  elfunsg  33955  dfrecs2  33989  dfrdg4  33990
  Copyright terms: Public domain W3C validator