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 𝐴 )