Theorem poss 2129

Description: Subset theorem for the partial ordering predicate.

Assertion

Ref	Expression
poss	⊢ (A ⊆ B → (R Po B → R Po A))

Proof of Theorem poss

Step	Hyp	Ref	Expression
1		ssel 1502	. . . . . . . . . 10 ⊢ (A ⊆ B → (x ∈ A → x ∈ B))
2		ssel 1502	. . . . . . . . . 10 ⊢ (A ⊆ B → (y ∈ A → y ∈ B))
3	1, 2	anim12d 431	. . . . . . . . 9 ⊢ (A ⊆ B → ((x ∈ A ∧ y ∈ A) → (x ∈ B ∧ y ∈ B)))
4		ssel 1502	. . . . . . . . 9 ⊢ (A ⊆ B → (z ∈ A → z ∈ B))
5	3, 4	anim12d 431	. . . . . . . 8 ⊢ (A ⊆ B → (((x ∈ A ∧ y ∈ A) ∧ z ∈ A) → ((x ∈ B ∧ y ∈ B) ∧ z ∈ B)))
6		df-3an 583	. . . . . . . 8 ⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) ↔ ((x ∈ A ∧ y ∈ A) ∧ z ∈ A))
7		df-3an 583	. . . . . . . 8 ⊢ ((x ∈ B ∧ y ∈ B ∧ z ∈ B) ↔ ((x ∈ B ∧ y ∈ B) ∧ z ∈ B))
8	5, 6, 7	3imtr4g 426	. . . . . . 7 ⊢ (A ⊆ B → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x ∈ B ∧ y ∈ B ∧ z ∈ B)))
9	8	syl4d 28	. . . . . 6 ⊢ (A ⊆ B → (((x ∈ B ∧ y ∈ B ∧ z ∈ B) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))) → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
10	9	19.20dv 946	. . . . 5 ⊢ (A ⊆ B → (∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))) → ∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
11	10	19.20dv 946	. . . 4 ⊢ (A ⊆ B → (∀y∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))) → ∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
12	11	19.20dv 946	. . 3 ⊢ (A ⊆ B → (∀x∀y∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))) → ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))))
13		r3al 1240	. . 3 ⊢ (∀x ∈ B ∀y ∈ B ∀z ∈ B (¬ xRx ∧ ((xRy ∧ yRz) → xRz)) ↔ ∀x∀y∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))))
14		r3al 1240	. . 3 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz)) ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (¬ xRx ∧ ((xRy ∧ yRz) → xRz))))
15	12, 13, 14	3imtr4g 426	. 2 ⊢ (A ⊆ B → (∀x ∈ B ∀y ∈ B ∀z ∈ B (¬ xRx ∧ ((xRy ∧ yRz) → xRz)) → ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz))))
16		df-po 2128	. 2 ⊢ (R Po B ↔ ∀x ∈ B ∀y ∈ B ∀z ∈ B (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))
17		df-po 2128	. 2 ⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬ xRx ∧ ((xRy ∧ yRz) → xRz)))
18	15, 16, 17	3imtr4g 426	1 ⊢ (A ⊆ B → (R Po B → R Po A))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196   ∧ w3a 581  ∀wal 672   ∈ wcel 1092  ∀wral 1201   ⊆ wss 1487   class class class wbr 2054   Po wpo 2058

This theorem is referenced by:  poeq2 2131  soss 2140  zornlem6 3608

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-in 1491  df-ss 1492  df-po 2128

metamath.org