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

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 ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑋 𝑅 𝑌 }
pofun.2 ⊢ ( 𝑥 = 𝑦 → 𝑋 = 𝑌 )
Assertion pofun ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ) → 𝑆 Po 𝐴 )

Proof

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