Theorem bropopvvv 7779

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 7778	. . 3 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸))
2		simpl 485	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉)
3		bropopvvv.p	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓))
4	3	opabbidv 5125	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {⟨𝑓, 𝑝⟩ ∣ 𝜑} = {⟨𝑓, 𝑝⟩ ∣ 𝜓})
5	2, 2, 4	mpoeq123dv 7223	. . . . . . . 8 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
6		bropopvvv.o	. . . . . . . 8 ⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}))
7	5, 6	ovmpoga 7298	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (𝑉𝑂𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
8	7	dmeqd 5769	. . . . . 6 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → dom (𝑉𝑂𝐸) = dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}))
9	8	eleq2d 2898	. . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓})))
10		dmoprabss 7250	. . . . . . . 8 ⊢ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} ⊆ (𝑉 × 𝑉)
11	10	sseli 3963	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} → ⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉))
12		opelxp 5586	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉) ↔ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))
13		df-br 5060	. . . . . . . . . . . . 13 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ ⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵))
14		ne0i 4300	. . . . . . . . . . . . . 14 ⊢ (⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅)
15		bropopvvv.oo	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ 𝜃})
16	15	breqd 5070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 ↔ 𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃))
17		brabv 5446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → (𝐹 ∈ V ∧ 𝑃 ∈ V))
18	17	anim2i 618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
19	18	ex 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
20	19	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹{⟨𝑓, 𝑝⟩ ∣ 𝜃}𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
21	16, 20	sylbid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
22	21	ex 415	. . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉𝑂𝐸) = ∅)
26		df-ov 7153	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴(𝑉𝑂𝐸)𝐵) = ((𝑉𝑂𝐸)‘⟨𝐴, 𝐵⟩)
27		fveq1 6664	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉𝑂𝐸) = ∅ → ((𝑉𝑂𝐸)‘⟨𝐴, 𝐵⟩) = (∅‘⟨𝐴, 𝐵⟩))
28	26, 27	syl5eq 2868	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = (∅‘⟨𝐴, 𝐵⟩))
29		0fv 6704	. . . . . . . . . . . . . . . . 17 ⊢ (∅‘⟨𝐴, 𝐵⟩) = ∅
30	28, 29	syl6eq 2872	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉𝑂𝐸) = ∅ → (𝐴(𝑉𝑂𝐸)𝐵) = ∅)
31		eqneqall 3027	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴(𝑉𝑂𝐸)𝐵) = ∅ → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))))
32	25, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))))
33	24, 32	pm2.61i 184	. . . . . . . . . . . . . 14 ⊢ ((𝐴(𝑉𝑂𝐸)𝐵) ≠ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
34	14, 33	syl 17	. . . . . . . . . . . . 13 ⊢ (⟨𝐹, 𝑃⟩ ∈ (𝐴(𝑉𝑂𝐸)𝐵) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))))
35	13, 34	sylbi 219	. . . . . . . . . . . 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 559	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
39		df-3an 1085	. . . . . . . . 9 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ↔ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))
40	38, 39	syl6ibr 254	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
41	12, 40	sylbi 219	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑉 × 𝑉) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
42	11, 41	syl 17	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})} → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
43		df-mpo 7155	. . . . . . 7 ⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})}
44	43	dmeqi 5768	. . . . . 6 ⊢ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) = dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {⟨𝑓, 𝑝⟩ ∣ 𝜓})}
45	42, 44	eleq2s 2931	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
46	9, 45	syl6bi 255	. . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
47		3ianor 1103	. . . . 5 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V))
48		df-3or 1084	. . . . . 6 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V))
49		ianor 978	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
50	25	dmeqd 5769	. . . . . . . . . . 11 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉𝑂𝐸) = dom ∅)
51	50	eleq2d 2898	. . . . . . . . . 10 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ dom ∅))
52		dm0 5785	. . . . . . . . . . 11 ⊢ dom ∅ = ∅
53	52	eleq2i 2904	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom ∅ ↔ ⟨𝐴, 𝐵⟩ ∈ ∅)
54	51, 53	syl6bb 289	. . . . . . . . 9 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) ↔ ⟨𝐴, 𝐵⟩ ∈ ∅))
55		noel 4296	. . . . . . . . . 10 ⊢ ¬ ⟨𝐴, 𝐵⟩ ∈ ∅
56	55	pm2.21i 119	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐵⟩ ∈ ∅ → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
57	54, 56	syl6bi 255	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
58	49, 57	sylbir 237	. . . . . . 7 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
59		anor 979	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ ¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
60		id 22	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ V → 𝑉 ∈ V)
61	60	ancri 552	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ V → (𝑉 ∈ V ∧ 𝑉 ∈ V))
62	61	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝑉 ∈ V))
63		mpoexga 7769	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V)
64	62, 63	syl 17	. . . . . . . . . 10 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V)
65	64	pm2.24d 154	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))))
66	59, 65	sylbir 237	. . . . . . . 8 ⊢ (¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))))
67	66	imp 409	. . . . . . 7 ⊢ ((¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∧ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
68	58, 67	jaoi3 1055	. . . . . 6 ⊢ (((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
69	48, 68	sylbi 219	. . . . 5 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜓}) ∈ V) → (⟨𝐴, 𝐵⟩ ∈ dom (𝑉𝑂𝐸) → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))))
70	47, 69	sylbi 219	. . . 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 17	. 2 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))))
73	72	pm2.43i 52	1 ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∨ w3o 1082   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  Vcvv 3495  ∅c0 4291  ⟨cop 4567   class class class wbr 5059  {copab 5121   × cxp 5548  dom cdm 5550  ‘cfv 6350  (class class class)co 7150  {coprab 7151   ∈ cmpo 7152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684

This theorem is referenced by: (None)