Step | Hyp | Ref
| Expression |
1 | | brovpreldm 7927 |
. . 3
⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → 〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸)) |
2 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉) |
3 | | bropopvvv.p |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓)) |
4 | 3 | opabbidv 5142 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {〈𝑓, 𝑝〉 ∣ 𝜑} = {〈𝑓, 𝑝〉 ∣ 𝜓}) |
5 | 2, 2, 4 | mpoeq123dv 7350 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ 𝜑}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓})) |
6 | | bropopvvv.o |
. . . . . . . 8
⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ 𝜑})) |
7 | 5, 6 | ovmpoga 7427 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (𝑉𝑂𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓})) |
8 | 7 | dmeqd 5816 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → dom (𝑉𝑂𝐸) = dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓})) |
9 | 8 | eleq2d 2824 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) ↔ 〈𝐴, 𝐵〉 ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}))) |
10 | | dmoprabss 7377 |
. . . . . . . 8
⊢ dom
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {〈𝑓, 𝑝〉 ∣ 𝜓})} ⊆ (𝑉 × 𝑉) |
11 | 10 | sseli 3918 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ dom
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {〈𝑓, 𝑝〉 ∣ 𝜓})} → 〈𝐴, 𝐵〉 ∈ (𝑉 × 𝑉)) |
12 | | opelxp 5627 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ (𝑉 × 𝑉) ↔ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
13 | | df-br 5077 |
. . . . . . . . . . . . 13
⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ 〈𝐹, 𝑃〉 ∈ (𝐴(𝑉𝑂𝐸)𝐵)) |
14 | | ne0i 4270 |
. . . . . . . . . . . . . 14
⊢
(〈𝐹, 𝑃〉 ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅) |
15 | | bropopvvv.oo |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ 𝜃}) |
16 | 15 | breqd 5087 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ 𝐹{〈𝑓, 𝑝〉 ∣ 𝜃}𝑃)) |
17 | | brabv 5484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹{〈𝑓, 𝑝〉 ∣ 𝜃}𝑃 → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
18 | 17 | anim2i 617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝐹{〈𝑓, 𝑝〉 ∣ 𝜃}𝑃) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
19 | 18 | ex 413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝐹{〈𝑓, 𝑝〉 ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹{〈𝑓, 𝑝〉 ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
21 | 16, 20 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
22 | 21 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))) |
23 | 22 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))) |
24 | 23 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))) |
25 | 6 | mpondm0 7510 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉𝑂𝐸) = ∅) |
26 | | df-ov 7280 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴(𝑉𝑂𝐸)𝐵) = ((𝑉𝑂𝐸)‘〈𝐴, 𝐵〉) |
27 | | fveq1 6775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉𝑂𝐸) = ∅ → ((𝑉𝑂𝐸)‘〈𝐴, 𝐵〉) = (∅‘〈𝐴, 𝐵〉)) |
28 | 26, 27 | eqtrid 2790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = (∅‘〈𝐴, 𝐵〉)) |
29 | | 0fv 6815 |
. . . . . . . . . . . . . . . . 17
⊢
(∅‘〈𝐴, 𝐵〉) = ∅ |
30 | 28, 29 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = ∅) |
31 | | eqneqall 2954 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴(𝑉𝑂𝐸)𝐵) = ∅ → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))) |
32 | 25, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))) |
33 | 24, 32 | pm2.61i 182 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))) |
34 | 14, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢
(〈𝐹, 𝑃〉 ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))) |
35 | 13, 34 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))) |
36 | 35 | pm2.43i 52 |
. . . . . . . . . . 11
⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
37 | 36 | com12 32 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
38 | 37 | anc2ri 557 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
39 | | df-3an 1088 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ↔ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
40 | 38, 39 | syl6ibr 251 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
41 | 12, 40 | sylbi 216 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ (𝑉 × 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
42 | 11, 41 | syl 17 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ dom
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {〈𝑓, 𝑝〉 ∣ 𝜓})} → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
43 | | df-mpo 7282 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) = {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {〈𝑓, 𝑝〉 ∣ 𝜓})} |
44 | 43 | dmeqi 5815 |
. . . . . 6
⊢ dom
(𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) = dom {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {〈𝑓, 𝑝〉 ∣ 𝜓})} |
45 | 42, 44 | eleq2s 2857 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
46 | 9, 45 | syl6bi 252 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
47 | | 3ianor 1106 |
. . . . 5
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V)) |
48 | | df-3or 1087 |
. . . . . 6
⊢ ((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V)) |
49 | | ianor 979 |
. . . . . . . 8
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V)) |
50 | 25 | dmeqd 5816 |
. . . . . . . . . . 11
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉𝑂𝐸) = dom ∅) |
51 | 50 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) ↔ 〈𝐴, 𝐵〉 ∈ dom ∅)) |
52 | | dm0 5831 |
. . . . . . . . . . 11
⊢ dom
∅ = ∅ |
53 | 52 | eleq2i 2830 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐵〉 ∈ dom ∅ ↔
〈𝐴, 𝐵〉 ∈ ∅) |
54 | 51, 53 | bitrdi 287 |
. . . . . . . . 9
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) ↔ 〈𝐴, 𝐵〉 ∈ ∅)) |
55 | | noel 4266 |
. . . . . . . . . 10
⊢ ¬
〈𝐴, 𝐵〉 ∈ ∅ |
56 | 55 | pm2.21i 119 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ ∅ →
(𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
57 | 54, 56 | syl6bi 252 |
. . . . . . . 8
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
58 | 49, 57 | sylbir 234 |
. . . . . . 7
⊢ ((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
59 | | anor 980 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ ¬ (¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V)) |
60 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ V → 𝑉 ∈ V) |
61 | 60 | ancri 550 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ V → (𝑉 ∈ V ∧ 𝑉 ∈ V)) |
62 | 61 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝑉 ∈ V)) |
63 | | mpoexga 7918 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) |
65 | 64 | pm2.24d 151 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))) |
66 | 59, 65 | sylbir 234 |
. . . . . . . 8
⊢ (¬
(¬ 𝑉 ∈ V ∨
¬ 𝐸 ∈ V) →
(¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))) |
67 | 66 | imp 407 |
. . . . . . 7
⊢ ((¬
(¬ 𝑉 ∈ V ∨
¬ 𝐸 ∈ V) ∧
¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
68 | 58, 67 | jaoi3 1058 |
. . . . . 6
⊢ (((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
69 | 48, 68 | sylbi 216 |
. . . . 5
⊢ ((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
70 | 47, 69 | sylbi 216 |
. . . 4
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {〈𝑓, 𝑝〉 ∣ 𝜓}) ∈ V) → (〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))) |
71 | 46, 70 | pm2.61i 182 |
. . 3
⊢
(〈𝐴, 𝐵〉 ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
72 | 1, 71 | syl 17 |
. 2
⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))) |
73 | 72 | pm2.43i 52 |
1
⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |