Theorem pofun 4975

Description: A function preserves a partial order relation. (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 3515	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋
2	1	nfel1 2765	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵
3		csbeq1a 3508	. . . . . . 7 ⊢ (𝑥 = 𝑣 → 𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
4	3	eleq1d 2672	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝑋 ∈ 𝐵 ↔ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
5	2, 4	rspc 3276	. . . . 5 ⊢ (𝑣 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
6	5	impcom 445	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵)
7		poirr 4970	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
8		df-br 4584	. . . . . 6 ⊢ (𝑣𝑆𝑣 ↔ ⟨𝑣, 𝑣⟩ ∈ 𝑆)
9		pofun.1	. . . . . . 7 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}
10	9	eleq2i 2680	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
11		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑥𝑅
12		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑥𝑌
13	1, 11, 12	nfbr 4629	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋𝑅𝑌
14		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋
15		vex 3176	. . . . . . 7 ⊢ 𝑣 ∈ V
16	3	breq1d 4593	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅𝑌))
17		vex 3176	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18		pofun.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)
19	17, 18	csbie 3525	. . . . . . . . 9 ⊢ ⦋𝑦 / 𝑥⦌𝑋 = 𝑌
20		csbeq1 3502	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
21	19, 20	syl5eqr 2658	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → 𝑌 = ⦋𝑣 / 𝑥⦌𝑋)
22	21	breq2d 4595	. . . . . . 7 ⊢ (𝑦 = 𝑣 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋))
23	13, 14, 15, 15, 16, 22	opelopabf 4925	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
24	8, 10, 23	3bitri 285	. . . . 5 ⊢ (𝑣𝑆𝑣 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
25	7, 24	sylnibr 318	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ 𝑣𝑆𝑣)
26	6, 25	sylan2 490	. . 3 ⊢ ((𝑅 Po 𝐵 ∧ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴)) → ¬ 𝑣𝑆𝑣)
27	26	anassrs 678	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ 𝑣 ∈ 𝐴) → ¬ 𝑣𝑆𝑣)
28	5	com12 32	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
29		nfcsb1v 3515	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋
30	29	nfel1 2765	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵
31		csbeq1a 3508	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → 𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
32	31	eleq1d 2672	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋 ∈ 𝐵 ↔ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
33	30, 32	rspc 3276	. . . . . . 7 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
34	33	com12 32	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑤 ∈ 𝐴 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
35		nfcsb1v 3515	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋
36	35	nfel1 2765	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵
37		csbeq1a 3508	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
38	37	eleq1d 2672	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑋 ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
39	36, 38	rspc 3276	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
40	39	com12 32	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑧 ∈ 𝐴 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
41	28, 34, 40	3anim123d 1398	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)))
42	41	imp 444	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
43	42	adantll 746	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
44		potr 4971	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋) → ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
45		df-br 4584	. . . . . . 7 ⊢ (𝑣𝑆𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑆)
46	9	eleq2i 2680	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
47		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋
48		vex 3176	. . . . . . . 8 ⊢ 𝑤 ∈ V
49		csbeq1 3502	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
50	19, 49	syl5eqr 2658	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → 𝑌 = ⦋𝑤 / 𝑥⦌𝑋)
51	50	breq2d 4595	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋))
52	13, 47, 15, 48, 16, 51	opelopabf 4925	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
53	45, 46, 52	3bitri 285	. . . . . 6 ⊢ (𝑣𝑆𝑤 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
54		df-br 4584	. . . . . . 7 ⊢ (𝑤𝑆𝑧 ↔ ⟨𝑤, 𝑧⟩ ∈ 𝑆)
55	9	eleq2i 2680	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
56	29, 11, 12	nfbr 4629	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋𝑅𝑌
57		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
58		vex 3176	. . . . . . . 8 ⊢ 𝑧 ∈ V
59	31	breq1d 4593	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅𝑌))
60		csbeq1 3502	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
61	19, 60	syl5eqr 2658	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝑌 = ⦋𝑧 / 𝑥⦌𝑋)
62	61	breq2d 4595	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (⦋𝑤 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
63	56, 57, 48, 58, 59, 62	opelopabf 4925	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
64	54, 55, 63	3bitri 285	. . . . . 6 ⊢ (𝑤𝑆𝑧 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
65	53, 64	anbi12i 729	. . . . 5 ⊢ ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) ↔ (⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
66		df-br 4584	. . . . . 6 ⊢ (𝑣𝑆𝑧 ↔ ⟨𝑣, 𝑧⟩ ∈ 𝑆)
67	9	eleq2i 2680	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
68		nfv 1830	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
69	61	breq2d 4595	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
70	13, 68, 15, 58, 16, 69	opelopabf 4925	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
71	66, 67, 70	3bitri 285	. . . . 5 ⊢ (𝑣𝑆𝑧 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
72	44, 65, 71	3imtr4g 284	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
73	72	adantlr 747	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
74	43, 73	syldan 486	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
75	27, 74	ispod 4967	1 ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ⦋csb 3499  ⟨cop 4131   class class class wbr 4583  {copab 4642   Po wpo 4957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-po 4959

This theorem is referenced by: (None)