Metamath Proof Explorer

Theorem pofun

Description: The inverse image of a partial order is a partial order. (Contributed by Jeff Madsen, 18-Jun-2011)

Ref Expression
Hypotheses pofun.1 ⊢ S = x y | X R Y
pofun.2 ⊢ x = y → X = Y
Assertion pofun ⊢ R Po B ∧ ∀ x ∈ A X ∈ B → S Po A

Proof

Step Hyp Ref Expression
1 pofun.1 ⊢ S = x y | X R Y
2 pofun.2 ⊢ x = y → X = Y
3 nfcsb1v ⊢ Ⅎ _ x ⦋ v / x⦌ X
4 3 nfel1 ⊢ Ⅎ x ⦋ v / x⦌ X ∈ B
5 csbeq1a ⊢ x = v → X = ⦋ v / x⦌ X
6 5 eleq1d ⊢ x = v → X ∈ B ↔ ⦋ v / x⦌ X ∈ B
7 4 6 rspc ⊢ v ∈ A → ∀ x ∈ A X ∈ B → ⦋ v / x⦌ X ∈ B
8 7 impcom ⊢ ∀ x ∈ A X ∈ B ∧ v ∈ A → ⦋ v / x⦌ X ∈ B
9 poirr ⊢ R Po B ∧ ⦋ v / x⦌ X ∈ B → ¬ ⦋ v / x⦌ X R ⦋ v / x⦌ X
10 df-br ⊢ v S v ↔ v v ∈ S
11 1 eleq2i ⊢ v v ∈ S ↔ v v ∈ x y | X R Y
12 nfcv ⊢ Ⅎ _ x R
13 nfcv ⊢ Ⅎ _ x Y
14 3 12 13 nfbr ⊢ Ⅎ x ⦋ v / x⦌ X R Y
15 nfv ⊢ Ⅎ y ⦋ v / x⦌ X R ⦋ v / x⦌ X
16 vex ⊢ v ∈ V
17 5 breq1d ⊢ x = v → X R Y ↔ ⦋ v / x⦌ X R Y
18 vex ⊢ y ∈ V
19 18 2 csbie ⊢ ⦋ y / x⦌ X = Y
20 csbeq1 ⊢ y = v → ⦋ y / x⦌ X = ⦋ v / x⦌ X
21 19 20 eqtr3id ⊢ y = v → Y = ⦋ v / x⦌ X
22 21 breq2d ⊢ y = v → ⦋ v / x⦌ X R Y ↔ ⦋ v / x⦌ X R ⦋ v / x⦌ X
23 14 15 16 16 17 22 opelopabf ⊢ v v ∈ x y | X R Y ↔ ⦋ v / x⦌ X R ⦋ v / x⦌ X
24 10 11 23 3bitri ⊢ v S v ↔ ⦋ v / x⦌ X R ⦋ v / x⦌ X
25 9 24 sylnibr ⊢ R Po B ∧ ⦋ v / x⦌ X ∈ B → ¬ v S v
26 8 25 sylan2 ⊢ R Po B ∧ ∀ x ∈ A X ∈ B ∧ v ∈ A → ¬ v S v
27 26 anassrs ⊢ R Po B ∧ ∀ x ∈ A X ∈ B ∧ v ∈ A → ¬ v S v
28 7 com12 ⊢ ∀ x ∈ A X ∈ B → v ∈ A → ⦋ v / x⦌ X ∈ B
29 nfcsb1v ⊢ Ⅎ _ x ⦋ w / x⦌ X
30 29 nfel1 ⊢ Ⅎ x ⦋ w / x⦌ X ∈ B
31 csbeq1a ⊢ x = w → X = ⦋ w / x⦌ X
32 31 eleq1d ⊢ x = w → X ∈ B ↔ ⦋ w / x⦌ X ∈ B
33 30 32 rspc ⊢ w ∈ A → ∀ x ∈ A X ∈ B → ⦋ w / x⦌ X ∈ B
34 33 com12 ⊢ ∀ x ∈ A X ∈ B → w ∈ A → ⦋ w / x⦌ X ∈ B
35 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ X
36 35 nfel1 ⊢ Ⅎ x ⦋ z / x⦌ X ∈ B
37 csbeq1a ⊢ x = z → X = ⦋ z / x⦌ X
38 37 eleq1d ⊢ x = z → X ∈ B ↔ ⦋ z / x⦌ X ∈ B
39 36 38 rspc ⊢ z ∈ A → ∀ x ∈ A X ∈ B → ⦋ z / x⦌ X ∈ B
40 39 com12 ⊢ ∀ x ∈ A X ∈ B → z ∈ A → ⦋ z / x⦌ X ∈ B
41 28 34 40 3anim123d ⊢ ∀ x ∈ A X ∈ B → v ∈ A ∧ w ∈ A ∧ z ∈ A → ⦋ v / x⦌ X ∈ B ∧ ⦋ w / x⦌ X ∈ B ∧ ⦋ z / x⦌ X ∈ B
42 41 imp ⊢ ∀ x ∈ A X ∈ B ∧ v ∈ A ∧ w ∈ A ∧ z ∈ A → ⦋ v / x⦌ X ∈ B ∧ ⦋ w / x⦌ X ∈ B ∧ ⦋ z / x⦌ X ∈ B
43 42 adantll ⊢ R Po B ∧ ∀ x ∈ A X ∈ B ∧ v ∈ A ∧ w ∈ A ∧ z ∈ A → ⦋ v / x⦌ X ∈ B ∧ ⦋ w / x⦌ X ∈ B ∧ ⦋ z / x⦌ X ∈ B
44 potr ⊢ R Po B ∧ ⦋ v / x⦌ X ∈ B ∧ ⦋ w / x⦌ X ∈ B ∧ ⦋ z / x⦌ X ∈ B → ⦋ v / x⦌ X R ⦋ w / x⦌ X ∧ ⦋ w / x⦌ X R ⦋ z / x⦌ X → ⦋ v / x⦌ X R ⦋ z / x⦌ X
45 df-br ⊢ v S w ↔ v w ∈ S
46 1 eleq2i ⊢ v w ∈ S ↔ v w ∈ x y | X R Y
47 nfv ⊢ Ⅎ y ⦋ v / x⦌ X R ⦋ w / x⦌ X
48 vex ⊢ w ∈ V
49 csbeq1 ⊢ y = w → ⦋ y / x⦌ X = ⦋ w / x⦌ X
50 19 49 eqtr3id ⊢ y = w → Y = ⦋ w / x⦌ X
51 50 breq2d ⊢ y = w → ⦋ v / x⦌ X R Y ↔ ⦋ v / x⦌ X R ⦋ w / x⦌ X
52 14 47 16 48 17 51 opelopabf ⊢ v w ∈ x y | X R Y ↔ ⦋ v / x⦌ X R ⦋ w / x⦌ X
53 45 46 52 3bitri ⊢ v S w ↔ ⦋ v / x⦌ X R ⦋ w / x⦌ X
54 df-br ⊢ w S z ↔ w z ∈ S
55 1 eleq2i ⊢ w z ∈ S ↔ w z ∈ x y | X R Y
56 29 12 13 nfbr ⊢ Ⅎ x ⦋ w / x⦌ X R Y
57 nfv ⊢ Ⅎ y ⦋ w / x⦌ X R ⦋ z / x⦌ X
58 vex ⊢ z ∈ V
59 31 breq1d ⊢ x = w → X R Y ↔ ⦋ w / x⦌ X R Y
60 csbeq1 ⊢ y = z → ⦋ y / x⦌ X = ⦋ z / x⦌ X
61 19 60 eqtr3id ⊢ y = z → Y = ⦋ z / x⦌ X
62 61 breq2d ⊢ y = z → ⦋ w / x⦌ X R Y ↔ ⦋ w / x⦌ X R ⦋ z / x⦌ X
63 56 57 48 58 59 62 opelopabf ⊢ w z ∈ x y | X R Y ↔ ⦋ w / x⦌ X R ⦋ z / x⦌ X
64 54 55 63 3bitri ⊢ w S z ↔ ⦋ w / x⦌ X R ⦋ z / x⦌ X
65 53 64 anbi12i ⊢ v S w ∧ w S z ↔ ⦋ v / x⦌ X R ⦋ w / x⦌ X ∧ ⦋ w / x⦌ X R ⦋ z / x⦌ X
66 df-br ⊢ v S z ↔ v z ∈ S
67 1 eleq2i ⊢ v z ∈ S ↔ v z ∈ x y | X R Y
68 nfv ⊢ Ⅎ y ⦋ v / x⦌ X R ⦋ z / x⦌ X
69 61 breq2d ⊢ y = z → ⦋ v / x⦌ X R Y ↔ ⦋ v / x⦌ X R ⦋ z / x⦌ X
70 14 68 16 58 17 69 opelopabf ⊢ v z ∈ x y | X R Y ↔ ⦋ v / x⦌ X R ⦋ z / x⦌ X
71 66 67 70 3bitri ⊢ v S z ↔ ⦋ v / x⦌ X R ⦋ z / x⦌ X
72 44 65 71 3imtr4g ⊢ R Po B ∧ ⦋ v / x⦌ X ∈ B ∧ ⦋ w / x⦌ X ∈ B ∧ ⦋ z / x⦌ X ∈ B → v S w ∧ w S z → v S z
73 72 adantlr ⊢ R Po B ∧ ∀ x ∈ A X ∈ B ∧ ⦋ v / x⦌ X ∈ B ∧ ⦋ w / x⦌ X ∈ B ∧ ⦋ z / x⦌ X ∈ B → v S w ∧ w S z → v S z
74 43 73 syldan ⊢ R Po B ∧ ∀ x ∈ A X ∈ B ∧ v ∈ A ∧ w ∈ A ∧ z ∈ A → v S w ∧ w S z → v S z
75 27 74 ispod ⊢ R Po B ∧ ∀ x ∈ A X ∈ B → S Po A