Theorem pofun 4172

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 2985	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋
2	1	nfel1 2251	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵
3		csbeq1a 2963	. . . . . . 7 ⊢ (𝑥 = 𝑣 → 𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
4	3	eleq1d 2168	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝑋 ∈ 𝐵 ↔ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
5	2, 4	rspc 2738	. . . . 5 ⊢ (𝑣 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
6	5	impcom 124	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵)
7		poirr 4167	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
8		df-br 3876	. . . . . 6 ⊢ (𝑣𝑆𝑣 ↔ ⟨𝑣, 𝑣⟩ ∈ 𝑆)
9		pofun.1	. . . . . . 7 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}
10	9	eleq2i 2166	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
11		nfcv 2240	. . . . . . . 8 ⊢ Ⅎ𝑥𝑅
12		nfcv 2240	. . . . . . . 8 ⊢ Ⅎ𝑥𝑌
13	1, 11, 12	nfbr 3919	. . . . . . 7 ⊢ Ⅎ𝑥⦋𝑣 / 𝑥⦌𝑋𝑅𝑌
14		nfv 1476	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋
15		vex 2644	. . . . . . 7 ⊢ 𝑣 ∈ V
16	3	breq1d 3885	. . . . . . 7 ⊢ (𝑥 = 𝑣 → (𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅𝑌))
17		vex 2644	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
18		pofun.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)
19	17, 12, 18	csbief 2994	. . . . . . . . 9 ⊢ ⦋𝑦 / 𝑥⦌𝑋 = 𝑌
20		csbeq1 2958	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑣 / 𝑥⦌𝑋)
21	19, 20	syl5eqr 2146	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → 𝑌 = ⦋𝑣 / 𝑥⦌𝑋)
22	21	breq2d 3887	. . . . . . 7 ⊢ (𝑦 = 𝑣 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋))
23	13, 14, 15, 15, 16, 22	opelopabf 4134	. . . . . 6 ⊢ (⟨𝑣, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
24	8, 10, 23	3bitri 205	. . . . 5 ⊢ (𝑣𝑆𝑣 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑣 / 𝑥⦌𝑋)
25	7, 24	sylnibr 643	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵) → ¬ 𝑣𝑆𝑣)
26	6, 25	sylan2 282	. . 3 ⊢ ((𝑅 Po 𝐵 ∧ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴)) → ¬ 𝑣𝑆𝑣)
27	26	anassrs 395	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ 𝑣 ∈ 𝐴) → ¬ 𝑣𝑆𝑣)
28	5	com12 30	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑣 ∈ 𝐴 → ⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵))
29		nfcsb1v 2985	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋
30	29	nfel1 2251	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵
31		csbeq1a 2963	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → 𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
32	31	eleq1d 2168	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋 ∈ 𝐵 ↔ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
33	30, 32	rspc 2738	. . . . . . 7 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
34	33	com12 30	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑤 ∈ 𝐴 → ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵))
35		nfcsb1v 2985	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋
36	35	nfel1 2251	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵
37		csbeq1a 2963	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
38	37	eleq1d 2168	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑋 ∈ 𝐵 ↔ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
39	36, 38	rspc 2738	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
40	39	com12 30	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → (𝑧 ∈ 𝐴 → ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
41	28, 34, 40	3anim123d 1265	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)))
42	41	imp 123	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
43	42	adantll 463	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵))
44		potr 4168	. . . . 5 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋) → ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
45		df-br 3876	. . . . . . 7 ⊢ (𝑣𝑆𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑆)
46	9	eleq2i 2166	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
47		nfv 1476	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋
48		vex 2644	. . . . . . . 8 ⊢ 𝑤 ∈ V
49		csbeq1 2958	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑤 / 𝑥⦌𝑋)
50	19, 49	syl5eqr 2146	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → 𝑌 = ⦋𝑤 / 𝑥⦌𝑋)
51	50	breq2d 3887	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋))
52	13, 47, 15, 48, 16, 51	opelopabf 4134	. . . . . . 7 ⊢ (⟨𝑣, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
53	45, 46, 52	3bitri 205	. . . . . 6 ⊢ (𝑣𝑆𝑤 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋)
54		df-br 3876	. . . . . . 7 ⊢ (𝑤𝑆𝑧 ↔ ⟨𝑤, 𝑧⟩ ∈ 𝑆)
55	9	eleq2i 2166	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
56	29, 11, 12	nfbr 3919	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑋𝑅𝑌
57		nfv 1476	. . . . . . . 8 ⊢ Ⅎ𝑦⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
58		vex 2644	. . . . . . . 8 ⊢ 𝑧 ∈ V
59	31	breq1d 3885	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅𝑌))
60		csbeq1 2958	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝑋 = ⦋𝑧 / 𝑥⦌𝑋)
61	19, 60	syl5eqr 2146	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝑌 = ⦋𝑧 / 𝑥⦌𝑋)
62	61	breq2d 3887	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (⦋𝑤 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
63	56, 57, 48, 58, 59, 62	opelopabf 4134	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
64	54, 55, 63	3bitri 205	. . . . . 6 ⊢ (𝑤𝑆𝑧 ↔ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
65	53, 64	anbi12i 451	. . . . 5 ⊢ ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) ↔ (⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑤 / 𝑥⦌𝑋 ∧ ⦋𝑤 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
66		df-br 3876	. . . . . 6 ⊢ (𝑣𝑆𝑧 ↔ ⟨𝑣, 𝑧⟩ ∈ 𝑆)
67	9	eleq2i 2166	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ 𝑆 ↔ ⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌})
68		nfv 1476	. . . . . . 7 ⊢ Ⅎ𝑦⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋
69	61	breq2d 3887	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (⦋𝑣 / 𝑥⦌𝑋𝑅𝑌 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋))
70	13, 68, 15, 58, 16, 69	opelopabf 4134	. . . . . 6 ⊢ (⟨𝑣, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
71	66, 67, 70	3bitri 205	. . . . 5 ⊢ (𝑣𝑆𝑧 ↔ ⦋𝑣 / 𝑥⦌𝑋𝑅⦋𝑧 / 𝑥⦌𝑋)
72	44, 65, 71	3imtr4g 204	. . . 4 ⊢ ((𝑅 Po 𝐵 ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
73	72	adantlr 464	. . 3 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (⦋𝑣 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑤 / 𝑥⦌𝑋 ∈ 𝐵 ∧ ⦋𝑧 / 𝑥⦌𝑋 ∈ 𝐵)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
74	43, 73	syldan 278	. 2 ⊢ (((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑣𝑆𝑤 ∧ 𝑤𝑆𝑧) → 𝑣𝑆𝑧))
75	27, 74	ispod 4164	1 ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∧ w3a 930   = wceq 1299   ∈ wcel 1448  ∀wral 2375  ⦋csb 2955  ⟨cop 3477   class class class wbr 3875  {copab 3928   Po wpo 4154

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-sbc 2863  df-csb 2956  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876  df-opab 3930  df-po 4156

This theorem is referenced by: (None)