Metamath Proof Explorer


Theorem prtlem15

Description: Lemma for prter1 and prtex . (Contributed by Rodolfo Medina, 13-Oct-2010)

Ref Expression
Assertion prtlem15 ( Prt 𝐴 → ( ∃ 𝑥𝐴𝑦𝐴 ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ∃ 𝑧𝐴 ( 𝑢𝑧𝑣𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 anabs7 ( ( ( 𝑤𝑥𝑤𝑦 ) ∧ ( ( 𝑢𝑥𝑣𝑦 ) ∧ ( 𝑤𝑥𝑤𝑦 ) ) ) ↔ ( ( 𝑢𝑥𝑣𝑦 ) ∧ ( 𝑤𝑥𝑤𝑦 ) ) )
2 an43 ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) ↔ ( ( 𝑢𝑥𝑣𝑦 ) ∧ ( 𝑤𝑥𝑤𝑦 ) ) )
3 2 anbi2i ( ( ( 𝑤𝑥𝑤𝑦 ) ∧ ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) ) ↔ ( ( 𝑤𝑥𝑤𝑦 ) ∧ ( ( 𝑢𝑥𝑣𝑦 ) ∧ ( 𝑤𝑥𝑤𝑦 ) ) ) )
4 1 3 2 3bitr4ri ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) ↔ ( ( 𝑤𝑥𝑤𝑦 ) ∧ ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) ) )
5 prtlem14 ( Prt 𝐴 → ( ( 𝑥𝐴𝑦𝐴 ) → ( ( 𝑤𝑥𝑤𝑦 ) → 𝑥 = 𝑦 ) ) )
6 an3 ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ( 𝑢𝑥𝑣𝑦 ) )
7 elequ2 ( 𝑥 = 𝑦 → ( 𝑣𝑥𝑣𝑦 ) )
8 7 anbi2d ( 𝑥 = 𝑦 → ( ( 𝑢𝑥𝑣𝑥 ) ↔ ( 𝑢𝑥𝑣𝑦 ) ) )
9 6 8 syl5ibr ( 𝑥 = 𝑦 → ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ( 𝑢𝑥𝑣𝑥 ) ) )
10 5 9 syl8 ( Prt 𝐴 → ( ( 𝑥𝐴𝑦𝐴 ) → ( ( 𝑤𝑥𝑤𝑦 ) → ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ( 𝑢𝑥𝑣𝑥 ) ) ) ) )
11 10 imp4a ( Prt 𝐴 → ( ( 𝑥𝐴𝑦𝐴 ) → ( ( ( 𝑤𝑥𝑤𝑦 ) ∧ ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) ) → ( 𝑢𝑥𝑣𝑥 ) ) ) )
12 4 11 syl7bi ( Prt 𝐴 → ( ( 𝑥𝐴𝑦𝐴 ) → ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ( 𝑢𝑥𝑣𝑥 ) ) ) )
13 12 expdimp ( ( Prt 𝐴𝑥𝐴 ) → ( 𝑦𝐴 → ( ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ( 𝑢𝑥𝑣𝑥 ) ) ) )
14 13 rexlimdv ( ( Prt 𝐴𝑥𝐴 ) → ( ∃ 𝑦𝐴 ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ( 𝑢𝑥𝑣𝑥 ) ) )
15 14 reximdva ( Prt 𝐴 → ( ∃ 𝑥𝐴𝑦𝐴 ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ∃ 𝑥𝐴 ( 𝑢𝑥𝑣𝑥 ) ) )
16 elequ2 ( 𝑥 = 𝑧 → ( 𝑢𝑥𝑢𝑧 ) )
17 elequ2 ( 𝑥 = 𝑧 → ( 𝑣𝑥𝑣𝑧 ) )
18 16 17 anbi12d ( 𝑥 = 𝑧 → ( ( 𝑢𝑥𝑣𝑥 ) ↔ ( 𝑢𝑧𝑣𝑧 ) ) )
19 18 cbvrexvw ( ∃ 𝑥𝐴 ( 𝑢𝑥𝑣𝑥 ) ↔ ∃ 𝑧𝐴 ( 𝑢𝑧𝑣𝑧 ) )
20 15 19 syl6ib ( Prt 𝐴 → ( ∃ 𝑥𝐴𝑦𝐴 ( ( 𝑢𝑥𝑤𝑥 ) ∧ ( 𝑤𝑦𝑣𝑦 ) ) → ∃ 𝑧𝐴 ( 𝑢𝑧𝑣𝑧 ) ) )