Theorem bropopvvv 8085

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 8084	. . 3 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸))
2		simpl 487	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉)
3		bropopvvv.p	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓))
4	3	opabbidv 5181	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {⟨𝑓, 𝑝⟩ ∣ 𝜑} = {⟨𝑓, 𝑝⟩ ∣ 𝜓})
5	2, 2, 4	mpoeq123dv 7486	. . . . . . . 8 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
6		bropopvvv.o	. . . . . . . 8 ⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}))
7	5, 6	ovmpoga 7565	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (𝑉𝑂𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
8	7	dmeqd 5896	. . . . . 6 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → dom (𝑉𝑂𝐸) = dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
9	8	eleq2d 2855	. . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓})))
10		dmoprabss 7515	. . . . . . . 8 ⊢ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} ⊆ (𝑉 × 𝑉)
11	10	sseli 3941	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} → ⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉))
12		opelxp 5698	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉) ↔ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))
13		df-br 5114	. . . . . . . . . . . . 13 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ ⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵))
14		ne0i 4302	. . . . . . . . . . . . . 14 ⊢ (⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅)
15		bropopvvv.oo	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ 𝜃})
16	15	breqd 5124	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ 𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃))
17		brabv 5552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → (𝐹 ∈ V ∧ 𝑃 ∈ V))
18	17	anim2i 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
19	18	ex 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
20	19	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
21	16, 20	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
22	21	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
23	22	com23 87	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
24	23	a1d 26	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))))
25	6	mpondm0 7651	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉𝑂𝐸) = ∅)
26		df-ov 7414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴(𝑉𝑂𝐸)𝐵) = ((𝑉𝑂𝐸)‘⟨𝐴, 𝐵⟩)
27		fveq1 6881	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉𝑂𝐸) = ∅ → ((𝑉𝑂𝐸)‘⟨𝐴, 𝐵⟩) = (∅‘⟨𝐴, 𝐵⟩))
28	26, 27	eqtrid 2816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = (∅‘⟨𝐴, 𝐵⟩))
29		0fv 6923	. . . . . . . . . . . . . . . . 17 ⊢ (∅‘⟨𝐴, 𝐵⟩) = ∅
30	28, 29	eqtrdi 2820	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = ∅)
31		eqneqall 2975	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴(𝑉𝑂𝐸)𝐵) = ∅ → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))))
32	25, 30, 31	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))))
33	24, 32	pm2.61i 184	. . . . . . . . . . . . . 14 ⊢ ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
34	14, 33	syl 18	. . . . . . . . . . . . 13 ⊢ (⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
35	13, 34	sylbi 220	. . . . . . . . . . . 12 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
36	35	pm2.43i 53	. . . . . . . . . . 11 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
37	36	com12 33	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
38	37	anc2ri 565	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
39		df-3an 1103	. . . . . . . . 9 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ↔ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))
40	38, 39	imbitrrdi 255	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
41	12, 40	sylbi 220	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
42	11, 41	syl 18	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
43		df-mpo 7416	. . . . . . 7 ⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})}
44	43	dmeqi 5895	. . . . . 6 ⊢ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) = dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})}
45	42, 44	eleq2s 2887	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
46	9, 45	biimtrdi 256	. . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
47		3ianor 1122	. . . . 5 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V))
48		df-3or 1102	. . . . . 6 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V))
49		ianor 997	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
50	25	dmeqd 5896	. . . . . . . . . . 11 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉𝑂𝐸) = dom ∅)
51	50	eleq2d 2855	. . . . . . . . . 10 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ dom ∅))
52		dm0 5911	. . . . . . . . . . 11 ⊢ dom ∅ = ∅
53	52	eleq2i 2861	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom ∅ ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
54	51, 53	bitrdi 290	. . . . . . . . 9 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ ∅))
55		noel 4299	. . . . . . . . . 10 ⊢ ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
56	55	pm2.21i 120	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐵⟩ ∈ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
57	54, 56	biimtrdi 256	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
58	49, 57	sylbir 238	. . . . . . 7 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
59		anor 998	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ ¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
60		id 23	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ V → 𝑉 ∈ V)
61	60	ancri 558	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ V → (𝑉 ∈ V ∧ 𝑉 ∈ V))
62	61	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝑉 ∈ V))
63		mpoexga 8074	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V)
64	62, 63	syl 18	. . . . . . . . . 10 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V)
65	64	pm2.24d 152	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))))
66	59, 65	sylbir 238	. . . . . . . 8 ⊢ (¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))))
67	66	imp 411	. . . . . . 7 ⊢ ((¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∧ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
68	58, 67	jaoi3 1074	. . . . . 6 ⊢ (((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
69	48, 68	sylbi 220	. . . . 5 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
70	47, 69	sylbi 220	. . . 4 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
71	46, 70	pm2.61i 184	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
72	1, 71	syl 18	. 2 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
73	72	pm2.43i 53	1 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∨ w3o 1100   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  Vcvv 3463  ∅c0 4294  ⟨cop 4600   class class class wbr 5113  {copab 5177   × cxp 5660  dom cdm 5662  ‘cfv 6537  (class class class)co 7411  {coprab 7412   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987

This theorem is referenced by: (None)