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

Metamath Proof Explorer

Theorem bropfvvvvlem

Description: Lemma for bropfvvvv . (Contributed by AV, 31-Dec-2020) (Revised by AV, 16-Jan-2021)

Ref Expression
Hypotheses bropfvvvv.o ⊢ 𝑂 = ( 𝑎 ∈ 𝑈 ↦ ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) )
bropfvvvv.oo ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
Assertion bropfvvvvlem ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) ∧ 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) )

Proof

Step Hyp Ref Expression
1 bropfvvvv.o ⊢ 𝑂 = ( 𝑎 ∈ 𝑈 ↦ ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) )
2 bropfvvvv.oo ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
3 opelxp ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) ↔ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) )
4 brne0 ⊢ ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) ≠ ∅ )
5 2 3expb ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
6 5 breqd ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 ↔ 𝐷 { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } 𝐸 ) )
7 brabv ⊢ ( 𝐷 { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } 𝐸 → ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) )
8 7 anim2i ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐷 { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } 𝐸 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) )
9 8 ex ⊢ ( 𝐴 ∈ 𝑈 → ( 𝐷 { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) → ( 𝐷 { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
11 6 10 sylbid ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
12 11 ex ⊢ ( 𝐴 ∈ 𝑈 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
13 12 com23 ⊢ ( 𝐴 ∈ 𝑈 → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
14 13 a1d ⊢ ( 𝐴 ∈ 𝑈 → ( ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) ≠ ∅ → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
15 1 fvmptndm ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( 𝑂 ‘ 𝐴 ) = ∅ )
16 df-ov ⊢ ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = ( ( 𝑂 ‘ 𝐴 ) ‘ ⟨ 𝐵 , 𝐶 ⟩ )
17 fveq1 ⊢ ( ( 𝑂 ‘ 𝐴 ) = ∅ → ( ( 𝑂 ‘ 𝐴 ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = ( ∅ ‘ ⟨ 𝐵 , 𝐶 ⟩ ) )
18 16 17 eqtrid ⊢ ( ( 𝑂 ‘ 𝐴 ) = ∅ → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = ( ∅ ‘ ⟨ 𝐵 , 𝐶 ⟩ ) )
19 0fv ⊢ ( ∅ ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = ∅
20 18 19 eqtrdi ⊢ ( ( 𝑂 ‘ 𝐴 ) = ∅ → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = ∅ )
21 eqneqall ⊢ ( ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = ∅ → ( ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) ≠ ∅ → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
22 15 20 21 3syl ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) ≠ ∅ → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
23 14 22 pm2.61i ⊢ ( ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) ≠ ∅ → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
24 4 23 mpcom ⊢ ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
25 24 com12 ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
26 25 anc2ri ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) ) )
27 3anan32 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ) )
28 26 27 imbitrrdi ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
29 3 28 sylbi ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
30 29 imp ⊢ ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) ∧ 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) )