Theorem pofun 5521

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 3857	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋
2	1	nfel1 2923	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵
3		csbeq1a 3846	. . . . . . 7 ⊢ (𝑥 = 𝑣 → 𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
4	3	eleq1d 2823	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝑋 ∈ 𝐵 ↔ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
5	2, 4	rspc 3549	. . . . 5 ⊢ (𝑣 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
6	5	impcom 408	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵)
7		poirr 5515	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
8		df-br 5075	. . . . . 6 ⊢ (𝑣𝑆𝑣 ↔ ⟨𝑣, 𝑣⟩ ∈ 𝑆)
9		pofun.1	. . . . . . 7 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}
10	9	eleq2i 2830	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
11		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑥𝑅
12		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑥𝑌
13	1, 11, 12	nfbr 5121	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋𝑅𝑌
14		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋
15		vex 3436	. . . . . . 7 ⊢ 𝑣 ∈ V
16	3	breq1d 5084	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅𝑌))
17		vex 3436	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18		pofun.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)
19	17, 18	csbie 3868	. . . . . . . . 9 ⊢ ⦋𝑦 / 𝑥⦌𝑋 = 𝑌
20		csbeq1 3835	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
21	19, 20	eqtr3id 2792	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → 𝑌 = ⦋𝑣 / 𝑥⦌𝑋)
22	21	breq2d 5086	. . . . . . 7 ⊢ (𝑦 = 𝑣 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋))
23	13, 14, 15, 15, 16, 22	opelopabf 5458	. . . . . 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 468	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ 𝑣 ∈ 𝐴) → ¬ 𝑣𝑆𝑣)
28	5	com12 32	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
29		nfcsb1v 3857	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋
30	29	nfel1 2923	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵
31		csbeq1a 3846	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → 𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
32	31	eleq1d 2823	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋 ∈ 𝐵 ↔ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
33	30, 32	rspc 3549	. . . . . . 7 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
34	33	com12 32	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑤 ∈ 𝐴 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
35		nfcsb1v 3857	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋
36	35	nfel1 2923	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵
37		csbeq1a 3846	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
38	37	eleq1d 2823	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑋 ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
39	36, 38	rspc 3549	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
40	39	com12 32	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑧 ∈ 𝐴 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
41	28, 34, 40	3anim123d 1442	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)))
42	41	imp 407	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
43	42	adantll 711	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
44		potr 5516	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋) → ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
45		df-br 5075	. . . . . . 7 ⊢ (𝑣𝑆𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑆)
46	9	eleq2i 2830	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
47		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋
48		vex 3436	. . . . . . . 8 ⊢ 𝑤 ∈ V
49		csbeq1 3835	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
50	19, 49	eqtr3id 2792	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → 𝑌 = ⦋𝑤 / 𝑥⦌𝑋)
51	50	breq2d 5086	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋))
52	13, 47, 15, 48, 16, 51	opelopabf 5458	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
53	45, 46, 52	3bitri 297	. . . . . 6 ⊢ (𝑣𝑆𝑤 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
54		df-br 5075	. . . . . . 7 ⊢ (𝑤𝑆𝑧 ↔ ⟨𝑤, 𝑧⟩ ∈ 𝑆)
55	9	eleq2i 2830	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
56	29, 11, 12	nfbr 5121	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋𝑅𝑌
57		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
58		vex 3436	. . . . . . . 8 ⊢ 𝑧 ∈ V
59	31	breq1d 5084	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅𝑌))
60		csbeq1 3835	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
61	19, 60	eqtr3id 2792	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝑌 = ⦋𝑧 / 𝑥⦌𝑋)
62	61	breq2d 5086	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (⦋𝑤 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
63	56, 57, 48, 58, 59, 62	opelopabf 5458	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
64	54, 55, 63	3bitri 297	. . . . . 6 ⊢ (𝑤𝑆𝑧 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
65	53, 64	anbi12i 627	. . . . 5 ⊢ ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) ↔ (⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
66		df-br 5075	. . . . . 6 ⊢ (𝑣𝑆𝑧 ↔ ⟨𝑣, 𝑧⟩ ∈ 𝑆)
67	9	eleq2i 2830	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
68		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
69	61	breq2d 5086	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
70	13, 68, 15, 58, 16, 69	opelopabf 5458	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
71	66, 67, 70	3bitri 297	. . . . 5 ⊢ (𝑣𝑆𝑧 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
72	44, 65, 71	3imtr4g 296	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
73	72	adantlr 712	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
74	43, 73	syldan 591	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
75	27, 74	ispod 5512	1 ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ⦋csb 3832  ⟨cop 4567   class class class wbr 5074  {copab 5136   Po wpo 5501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-po 5503

This theorem is referenced by: (None)