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