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