Theorem prtlem18 38871

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

Hypothesis

Ref	Expression
prtlem18.1	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}

Assertion

Ref	Expression
prtlem18	⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))

Distinct variable groups:   𝑣,𝑢,𝑤,𝑥,𝑦,𝑧,𝐴   𝑣, ∼ ,𝑤,𝑧

Allowed substitution hints:   ∼ (𝑥,𝑦,𝑢)

Proof of Theorem prtlem18

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rspe 3248	. . . . 5 ⊢ ((𝑣 ∈ 𝐴 ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
2	1	expr 456	. . . 4 ⊢ ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 → ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
3		prtlem18.1	. . . . 5 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}
4	3	prtlem13 38862	. . . 4 ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
5	2, 4	imbitrrdi 252	. . 3 ⊢ ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 → 𝑧 ∼ 𝑤))
6	5	a1i 11	. 2 ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 → 𝑧 ∼ 𝑤)))
7	3	prtlem13 38862	. . 3 ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑝 ∈ 𝐴 (𝑧 ∈ 𝑝 ∧ 𝑤 ∈ 𝑝))
8		prtlem17 38870	. . 3 ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (∃𝑝 ∈ 𝐴 (𝑧 ∈ 𝑝 ∧ 𝑤 ∈ 𝑝) → 𝑤 ∈ 𝑣)))
9	7, 8	syl7bi 255	. 2 ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑧 ∼ 𝑤 → 𝑤 ∈ 𝑣)))
10	6, 9	impbidd 210	1 ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1538   ∈ wcel 2107  ∃wrex 3069   class class class wbr 5149  {copab 5211  Prt wprt 38865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2707  ax-sep 5303  ax-nul 5313  ax-pr 5439

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3435  df-v 3481  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-nul 4341  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5150  df-opab 5212  df-prt 38866

This theorem is referenced by:  prtlem19  38872