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

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 imbitrrid ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦 ) ) → ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥 ) ) )
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 imbitrdi ⊢ ( Prt 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧 ) ) )