Theorem pofun 5578

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 3879	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋
2	1	nfel1 2943	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵
3		csbeq1a 3869	. . . . . . 7 ⊢ (𝑥 = 𝑣 → 𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
4	3	eleq1d 2850	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝑋 ∈ 𝐵 ↔ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
5	2, 4	rspc 3572	. . . . 5 ⊢ (𝑣 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
6	5	impcom 412	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵)
7		poirr 5572	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
8		df-br 5106	. . . . . 6 ⊢ (𝑣𝑆𝑣 ↔ ⟨𝑣, 𝑣⟩ ∈ 𝑆)
9		pofun.1	. . . . . . 7 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}
10	9	eleq2i 2857	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
11		nfcv 2927	. . . . . . . 8 ⊢ Ⅎ𝑥𝑅
12		nfcv 2927	. . . . . . . 8 ⊢ Ⅎ𝑥𝑌
13	1, 11, 12	nfbr 5152	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋𝑅𝑌
14		nfv 1937	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋
15		vex 3461	. . . . . . 7 ⊢ 𝑣 ∈ V
16	3	breq1d 5115	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅𝑌))
17		vex 3461	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18		pofun.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)
19	17, 18	csbie 3890	. . . . . . . . 9 ⊢ ⦋𝑦 / 𝑥⦌𝑋 = 𝑌
20		csbeq1 3858	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
21	19, 20	eqtr3id 2814	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → 𝑌 = ⦋𝑣 / 𝑥⦌𝑋)
22	21	breq2d 5117	. . . . . . 7 ⊢ (𝑦 = 𝑣 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋))
23	13, 14, 15, 15, 16, 22	opelopabf 5521	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
24	8, 10, 23	3bitri 300	. . . . 5 ⊢ (𝑣𝑆𝑣 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
25	7, 24	sylnibr 332	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ 𝑣𝑆𝑣)
26	6, 25	sylan2 604	. . 3 ⊢ ((𝑅 Po 𝐵 ∧ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴)) → ¬ 𝑣𝑆𝑣)
27	26	anassrs 472	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ 𝑣 ∈ 𝐴) → ¬ 𝑣𝑆𝑣)
28	5	com12 33	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
29		nfcsb1v 3879	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋
30	29	nfel1 2943	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵
31		csbeq1a 3869	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → 𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
32	31	eleq1d 2850	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋 ∈ 𝐵 ↔ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
33	30, 32	rspc 3572	. . . . . . 7 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
34	33	com12 33	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑤 ∈ 𝐴 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
35		nfcsb1v 3879	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋
36	35	nfel1 2943	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵
37		csbeq1a 3869	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
38	37	eleq1d 2850	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑋 ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
39	36, 38	rspc 3572	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
40	39	com12 33	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑧 ∈ 𝐴 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
41	28, 34, 40	3anim123d 1467	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)))
42	41	imp 411	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
43	42	adantll 726	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
44		potr 5573	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋) → ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
45		df-br 5106	. . . . . . 7 ⊢ (𝑣𝑆𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑆)
46	9	eleq2i 2857	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
47		nfv 1937	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋
48		vex 3461	. . . . . . . 8 ⊢ 𝑤 ∈ V
49		csbeq1 3858	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
50	19, 49	eqtr3id 2814	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → 𝑌 = ⦋𝑤 / 𝑥⦌𝑋)
51	50	breq2d 5117	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋))
52	13, 47, 15, 48, 16, 51	opelopabf 5521	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
53	45, 46, 52	3bitri 300	. . . . . 6 ⊢ (𝑣𝑆𝑤 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
54		df-br 5106	. . . . . . 7 ⊢ (𝑤𝑆𝑧 ↔ ⟨𝑤, 𝑧⟩ ∈ 𝑆)
55	9	eleq2i 2857	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
56	29, 11, 12	nfbr 5152	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋𝑅𝑌
57		nfv 1937	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
58		vex 3461	. . . . . . . 8 ⊢ 𝑧 ∈ V
59	31	breq1d 5115	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅𝑌))
60		csbeq1 3858	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
61	19, 60	eqtr3id 2814	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝑌 = ⦋𝑧 / 𝑥⦌𝑋)
62	61	breq2d 5117	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (⦋𝑤 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
63	56, 57, 48, 58, 59, 62	opelopabf 5521	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
64	54, 55, 63	3bitri 300	. . . . . 6 ⊢ (𝑤𝑆𝑧 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
65	53, 64	anbi12i 639	. . . . 5 ⊢ ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) ↔ (⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
66		df-br 5106	. . . . . 6 ⊢ (𝑣𝑆𝑧 ↔ ⟨𝑣, 𝑧⟩ ∈ 𝑆)
67	9	eleq2i 2857	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
68		nfv 1937	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
69	61	breq2d 5117	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
70	13, 68, 15, 58, 16, 69	opelopabf 5521	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
71	66, 67, 70	3bitri 300	. . . . 5 ⊢ (𝑣𝑆𝑧 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
72	44, 65, 71	3imtr4g 299	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
73	72	adantlr 727	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
74	43, 73	syldan 602	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
75	27, 74	ispod 5569	1 ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ⦋csb 3855  ⟨cop 4591   class class class wbr 5105  {copab 5167   Po wpo 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-po 5560

This theorem is referenced by: (None)