Theorem pofun 5584

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

Hypotheses

Ref	Expression
pofun.1	⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}
pofun.2	⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)

Assertion

Ref	Expression
pofun	⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)

Distinct variable groups:   𝑥,𝑅,𝑦   𝑦,𝑋   𝑥,𝑌   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑦)   𝑆(𝑥,𝑦)   𝑋(𝑥)   𝑌(𝑦)

Proof of Theorem pofun

Dummy variables 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3052  ⦋csb 3879  ⟨cop 4612   class class class wbr 5124  {copab 5186   Po wpo 5564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-po 5566

This theorem is referenced by: (None)