Metamath Proof Explorer


Theorem prtlem18

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem18.1 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) }
Assertion prtlem18 ( Prt 𝐴 → ( ( 𝑣𝐴𝑧𝑣 ) → ( 𝑤𝑣𝑧 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 prtlem18.1 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) }
2 rspe ( ( 𝑣𝐴 ∧ ( 𝑧𝑣𝑤𝑣 ) ) → ∃ 𝑣𝐴 ( 𝑧𝑣𝑤𝑣 ) )
3 2 expr ( ( 𝑣𝐴𝑧𝑣 ) → ( 𝑤𝑣 → ∃ 𝑣𝐴 ( 𝑧𝑣𝑤𝑣 ) ) )
4 1 prtlem13 ( 𝑧 𝑤 ↔ ∃ 𝑣𝐴 ( 𝑧𝑣𝑤𝑣 ) )
5 3 4 syl6ibr ( ( 𝑣𝐴𝑧𝑣 ) → ( 𝑤𝑣𝑧 𝑤 ) )
6 5 a1i ( Prt 𝐴 → ( ( 𝑣𝐴𝑧𝑣 ) → ( 𝑤𝑣𝑧 𝑤 ) ) )
7 1 prtlem13 ( 𝑧 𝑤 ↔ ∃ 𝑝𝐴 ( 𝑧𝑝𝑤𝑝 ) )
8 prtlem17 ( Prt 𝐴 → ( ( 𝑣𝐴𝑧𝑣 ) → ( ∃ 𝑝𝐴 ( 𝑧𝑝𝑤𝑝 ) → 𝑤𝑣 ) ) )
9 7 8 syl7bi ( Prt 𝐴 → ( ( 𝑣𝐴𝑧𝑣 ) → ( 𝑧 𝑤𝑤𝑣 ) ) )
10 6 9 impbidd ( Prt 𝐴 → ( ( 𝑣𝐴𝑧𝑣 ) → ( 𝑤𝑣𝑧 𝑤 ) ) )