Theorem bropopvvv 8115

Description: If a binary relation holds for the result of an operation which is a result of an operation, the involved classes are sets. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Proof shortened by AV, 3-Jan-2021.)

Hypotheses

Ref	Expression
bropopvvv.o	⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}))
bropopvvv.p	⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓))
bropopvvv.oo	⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ 𝜃})

Assertion

Ref	Expression
bropopvvv	⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))

Distinct variable groups:   𝐸,𝑎,𝑏,𝑒,𝑓,𝑝,𝑣   𝑉,𝑎,𝑏,𝑒,𝑓,𝑝,𝑣   𝜓,𝑒,𝑣

Allowed substitution hints:   𝜑(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)   𝜓(𝑓,𝑝,𝑎,𝑏)   𝜃(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)   𝐴(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)   𝐵(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)   𝑃(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)   𝐹(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)   𝑂(𝑣,𝑒,𝑓,𝑝,𝑎,𝑏)

Proof of Theorem bropopvvv

Dummy variable 𝑐 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brovpreldm 8114	. . 3 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸))
2		simpl 482	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉)
3		bropopvvv.p	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓))
4	3	opabbidv 5209	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {⟨𝑓, 𝑝⟩ ∣ 𝜑} = {⟨𝑓, 𝑝⟩ ∣ 𝜓})
5	2, 2, 4	mpoeq123dv 7508	. . . . . . . 8 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
6		bropopvvv.o	. . . . . . . 8 ⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}))
7	5, 6	ovmpoga 7587	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (𝑉𝑂𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
8	7	dmeqd 5916	. . . . . 6 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → dom (𝑉𝑂𝐸) = dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
9	8	eleq2d 2827	. . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓})))
10		dmoprabss 7537	. . . . . . . 8 ⊢ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} ⊆ (𝑉 × 𝑉)
11	10	sseli 3979	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} → ⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉))
12		opelxp 5721	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉) ↔ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))
13		df-br 5144	. . . . . . . . . . . . 13 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ ⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵))
14		ne0i 4341	. . . . . . . . . . . . . 14 ⊢ (⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅)
15		bropopvvv.oo	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ 𝜃})
16	15	breqd 5154	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ 𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃))
17		brabv 5573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → (𝐹 ∈ V ∧ 𝑃 ∈ V))
18	17	anim2i 617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
19	18	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
20	19	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
21	16, 20	sylbid 240	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
22	21	ex 412	. . . . . . . . . . . . . . . . 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 7673	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉𝑂𝐸) = ∅)
26		df-ov 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴(𝑉𝑂𝐸)𝐵) = ((𝑉𝑂𝐸)‘⟨𝐴, 𝐵⟩)
27		fveq1 6905	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉𝑂𝐸) = ∅ → ((𝑉𝑂𝐸)‘⟨𝐴, 𝐵⟩) = (∅‘⟨𝐴, 𝐵⟩))
28	26, 27	eqtrid 2789	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = (∅‘⟨𝐴, 𝐵⟩))
29		0fv 6950	. . . . . . . . . . . . . . . . 17 ⊢ (∅‘⟨𝐴, 𝐵⟩) = ∅
30	28, 29	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = ∅)
31		eqneqall 2951	. . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . 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 556	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
39		df-3an 1089	. . . . . . . . 9 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ↔ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))
40	38, 39	imbitrrdi 252	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
41	12, 40	sylbi 217	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
42	11, 41	syl 17	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
43		df-mpo 7436	. . . . . . 7 ⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})}
44	43	dmeqi 5915	. . . . . 6 ⊢ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) = dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})}
45	42, 44	eleq2s 2859	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
46	9, 45	biimtrdi 253	. . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
47		3ianor 1107	. . . . 5 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V))
48		df-3or 1088	. . . . . 6 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V))
49		ianor 984	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
50	25	dmeqd 5916	. . . . . . . . . . 11 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉𝑂𝐸) = dom ∅)
51	50	eleq2d 2827	. . . . . . . . . 10 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ dom ∅))
52		dm0 5931	. . . . . . . . . . 11 ⊢ dom ∅ = ∅
53	52	eleq2i 2833	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom ∅ ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
54	51, 53	bitrdi 287	. . . . . . . . 9 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ ∅))
55		noel 4338	. . . . . . . . . 10 ⊢ ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
56	55	pm2.21i 119	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐵⟩ ∈ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
57	54, 56	biimtrdi 253	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
58	49, 57	sylbir 235	. . . . . . 7 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
59		anor 985	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ ¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
60		id 22	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ V → 𝑉 ∈ V)
61	60	ancri 549	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ V → (𝑉 ∈ V ∧ 𝑉 ∈ V))
62	61	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝑉 ∈ V))
63		mpoexga 8102	. . . . . . . . . . 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 235	. . . . . . . 8 ⊢ (¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))))
67	66	imp 406	. . . . . . 7 ⊢ ((¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∧ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
68	58, 67	jaoi3 1061	. . . . . 6 ⊢ (((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
69	48, 68	sylbi 217	. . . . 5 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
70	47, 69	sylbi 217	. . . 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) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480  ∅c0 4333  ⟨cop 4632   class class class wbr 5143  {copab 5205   × cxp 5683  dom cdm 5685  ‘cfv 6561  (class class class)co 7431  {coprab 7432   ∈ cmpo 7433

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-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  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-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  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-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015

This theorem is referenced by: (None)