Theorem bropopvvv

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)

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

Proof

Step	Hyp	Ref	Expression
1		bropopvvv.o	⊢ 𝑂 = ( 𝑣 ∈ V , 𝑒 ∈ V ↦ ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜑 } ) )
2		bropopvvv.p	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜑 ↔ 𝜓 ) )
3		bropopvvv.oo	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜃 } )
4		brovpreldm	⊢ ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) )
5		simpl	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → 𝑣 = 𝑉 )
6	2	opabbidv	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜑 } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } )
7	5 5 6	mpoeq123dv	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜑 } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) )
8	7 1	ovmpoga	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( 𝑉 𝑂 𝐸 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) )
9	8	dmeqd	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → dom ( 𝑉 𝑂 𝐸 ) = dom ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) )
10	9	eleq2d	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ) )
11		dmoprabss	⊢ dom { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) } ⊆ ( 𝑉 × 𝑉 )
12	11	sseli	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) } → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) )
13		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
14		df-br	⊢ ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) )
15		ne0i	⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) → ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) ≠ ∅ )
16	3	breqd	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 ↔ 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜃 } 𝑃 ) )
17		brabv	⊢ ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜃 } 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
18	17	anim2i	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜃 } 𝑃 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
19	18	ex	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜃 } 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
20	19	adantr	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜃 } 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
21	16 20	sylbid	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
22	21	ex	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) )
23	22	com23	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) )
24	23	a1d	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) ≠ ∅ → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) ) )
25	1	mpondm0	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝑉 𝑂 𝐸 ) = ∅ )
26		df-ov	⊢ ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) = ( ( 𝑉 𝑂 𝐸 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
27		fveq1	⊢ ( ( 𝑉 𝑂 𝐸 ) = ∅ → ( ( 𝑉 𝑂 𝐸 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ∅ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
28	26 27	eqtrid	⊢ ( ( 𝑉 𝑂 𝐸 ) = ∅ → ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) = ( ∅ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
29		0fv	⊢ ( ∅ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅
30	28 29	eqtrdi	⊢ ( ( 𝑉 𝑂 𝐸 ) = ∅ → ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) = ∅ )
31		eqneqall	⊢ ( ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) = ∅ → ( ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) ≠ ∅ → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) ) )
32	25 30 31	3syl	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) ≠ ∅ → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) ) )
33	24 32	pm2.61i	⊢ ( ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) ≠ ∅ → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) )
34	15 33	syl	⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) )
35	14 34	sylbi	⊢ ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) )
36	35	pm2.43i	⊢ ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
37	36	com12	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
38	37	anc2ri	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
39		df-3an	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ↔ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
40	38 39	imbitrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
41	13 40	sylbi	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
42	12 41	syl	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) } → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
43		df-mpo	⊢ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) }
44	43	dmeqi	⊢ dom ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) = dom { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑐 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) }
45	42 44	eleq2s	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
46	10 45	biimtrdi	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
47		3ianor	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) ↔ ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) )
48		df-3or	⊢ ( ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) ↔ ( ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) ∨ ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) )
49		ianor	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ↔ ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) )
50	25	dmeqd	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → dom ( 𝑉 𝑂 𝐸 ) = dom ∅ )
51	50	eleq2d	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ∅ ) )
52		dm0	⊢ dom ∅ = ∅
53	52	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ∅ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∅ )
54	51 53	bitrdi	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∅ ) )
55		noel	⊢ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∅
56	55	pm2.21i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ∅ → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
57	54 56	biimtrdi	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
58	49 57	sylbir	⊢ ( ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
59		anor	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ↔ ¬ ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) )
60		id	⊢ ( 𝑉 ∈ V → 𝑉 ∈ V )
61	60	ancri	⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ V ∧ 𝑉 ∈ V ) )
62	61	adantr	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝑉 ∈ V ∧ 𝑉 ∈ V ) )
63		mpoexga	⊢ ( ( 𝑉 ∈ V ∧ 𝑉 ∈ V ) → ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V )
64	62 63	syl	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V )
65	64	pm2.24d	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) ) )
66	59 65	sylbir	⊢ ( ¬ ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) → ( ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) ) )
67	66	imp	⊢ ( ( ¬ ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) ∧ ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
68	58 67	jaoi3	⊢ ( ( ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ) ∨ ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
69	48 68	sylbi	⊢ ( ( ¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
70	47 69	sylbi	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ) )
71	46 70	pm2.61i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
72	4 71	syl	⊢ ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
73	72	pm2.43i	⊢ ( 𝐹 ( 𝐴 ( 𝑉 𝑂 𝐸 ) 𝐵 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )