This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )