Theorem pofun 4040

Description: A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)

Hypotheses

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

Assertion

Ref	Expression
pofun	⊢ ((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) → 𝑆 Po A)

Distinct variable groups:   x,𝑅,y   y,𝑋   x,𝑌   x,A   x,B

Allowed substitution hints:   A(y)   B(y)   𝑆(x,y)   𝑋(x)   𝑌(y)

Proof of Theorem pofun

Dummy variables v w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcsb1v 2876	. . . . . . 7 ⊢ Ⅎx⦋v / x⦌𝑋
2	1	nfel1 2185	. . . . . 6 ⊢ Ⅎx⦋v / x⦌𝑋 ∈ B
3		csbeq1a 2854	. . . . . . 7 ⊢ (x = v → 𝑋 = ⦋v / x⦌𝑋)
4	3	eleq1d 2103	. . . . . 6 ⊢ (x = v → (𝑋 ∈ B ↔ ⦋v / x⦌𝑋 ∈ B))
5	2, 4	rspc 2644	. . . . 5 ⊢ (v ∈ A → (∀x ∈ A 𝑋 ∈ B → ⦋v / x⦌𝑋 ∈ B))
6	5	impcom 116	. . . 4 ⊢ ((∀x ∈ A 𝑋 ∈ B ∧ v ∈ A) → ⦋v / x⦌𝑋 ∈ B)
7		poirr 4035	. . . . 5 ⊢ ((𝑅 Po B ∧ ⦋v / x⦌𝑋 ∈ B) → ¬ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋)
8		df-br 3756	. . . . . 6 ⊢ (v𝑆v ↔ ⟨v, v⟩ ∈ 𝑆)
9		pofun.1	. . . . . . 7 ⊢ 𝑆 = {⟨x, y⟩ ∣ 𝑋𝑅𝑌}
10	9	eleq2i 2101	. . . . . 6 ⊢ (⟨v, v⟩ ∈ 𝑆 ↔ ⟨v, v⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌})
11		nfcv 2175	. . . . . . . 8 ⊢ Ⅎx𝑅
12		nfcv 2175	. . . . . . . 8 ⊢ Ⅎx𝑌
13	1, 11, 12	nfbr 3799	. . . . . . 7 ⊢ Ⅎx⦋v / x⦌𝑋𝑅𝑌
14		nfv 1418	. . . . . . 7 ⊢ Ⅎy⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋
15		vex 2554	. . . . . . 7 ⊢ v ∈ V
16	3	breq1d 3765	. . . . . . 7 ⊢ (x = v → (𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅𝑌))
17		vex 2554	. . . . . . . . . 10 ⊢ y ∈ V
18		pofun.2	. . . . . . . . . 10 ⊢ (x = y → 𝑋 = 𝑌)
19	17, 12, 18	csbief 2885	. . . . . . . . 9 ⊢ ⦋y / x⦌𝑋 = 𝑌
20		csbeq1 2849	. . . . . . . . 9 ⊢ (y = v → ⦋y / x⦌𝑋 = ⦋v / x⦌𝑋)
21	19, 20	syl5eqr 2083	. . . . . . . 8 ⊢ (y = v → 𝑌 = ⦋v / x⦌𝑋)
22	21	breq2d 3767	. . . . . . 7 ⊢ (y = v → (⦋v / x⦌𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋))
23	13, 14, 15, 15, 16, 22	opelopabf 4002	. . . . . 6 ⊢ (⟨v, v⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋)
24	8, 10, 23	3bitri 195	. . . . 5 ⊢ (v𝑆v ↔ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋)
25	7, 24	sylnibr 601	. . . 4 ⊢ ((𝑅 Po B ∧ ⦋v / x⦌𝑋 ∈ B) → ¬ v𝑆v)
26	6, 25	sylan2 270	. . 3 ⊢ ((𝑅 Po B ∧ (∀x ∈ A 𝑋 ∈ B ∧ v ∈ A)) → ¬ v𝑆v)
27	26	anassrs 380	. 2 ⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ v ∈ A) → ¬ v𝑆v)
28	5	com12 27	. . . . . 6 ⊢ (∀x ∈ A 𝑋 ∈ B → (v ∈ A → ⦋v / x⦌𝑋 ∈ B))
29		nfcsb1v 2876	. . . . . . . . 9 ⊢ Ⅎx⦋w / x⦌𝑋
30	29	nfel1 2185	. . . . . . . 8 ⊢ Ⅎx⦋w / x⦌𝑋 ∈ B
31		csbeq1a 2854	. . . . . . . . 9 ⊢ (x = w → 𝑋 = ⦋w / x⦌𝑋)
32	31	eleq1d 2103	. . . . . . . 8 ⊢ (x = w → (𝑋 ∈ B ↔ ⦋w / x⦌𝑋 ∈ B))
33	30, 32	rspc 2644	. . . . . . 7 ⊢ (w ∈ A → (∀x ∈ A 𝑋 ∈ B → ⦋w / x⦌𝑋 ∈ B))
34	33	com12 27	. . . . . 6 ⊢ (∀x ∈ A 𝑋 ∈ B → (w ∈ A → ⦋w / x⦌𝑋 ∈ B))
35		nfcsb1v 2876	. . . . . . . . 9 ⊢ Ⅎx⦋z / x⦌𝑋
36	35	nfel1 2185	. . . . . . . 8 ⊢ Ⅎx⦋z / x⦌𝑋 ∈ B
37		csbeq1a 2854	. . . . . . . . 9 ⊢ (x = z → 𝑋 = ⦋z / x⦌𝑋)
38	37	eleq1d 2103	. . . . . . . 8 ⊢ (x = z → (𝑋 ∈ B ↔ ⦋z / x⦌𝑋 ∈ B))
39	36, 38	rspc 2644	. . . . . . 7 ⊢ (z ∈ A → (∀x ∈ A 𝑋 ∈ B → ⦋z / x⦌𝑋 ∈ B))
40	39	com12 27	. . . . . 6 ⊢ (∀x ∈ A 𝑋 ∈ B → (z ∈ A → ⦋z / x⦌𝑋 ∈ B))
41	28, 34, 40	3anim123d 1213	. . . . 5 ⊢ (∀x ∈ A 𝑋 ∈ B → ((v ∈ A ∧ w ∈ A ∧ z ∈ A) → (⦋v / x⦌𝑋 ∈ B ∧ ⦋w / x⦌𝑋 ∈ B ∧ ⦋z / x⦌𝑋 ∈ B)))
42	41	imp 115	. . . 4 ⊢ ((∀x ∈ A 𝑋 ∈ B ∧ (v ∈ A ∧ w ∈ A ∧ z ∈ A)) → (⦋v / x⦌𝑋 ∈ B ∧ ⦋w / x⦌𝑋 ∈ B ∧ ⦋z / x⦌𝑋 ∈ B))
43	42	adantll 445	. . 3 ⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ (v ∈ A ∧ w ∈ A ∧ z ∈ A)) → (⦋v / x⦌𝑋 ∈ B ∧ ⦋w / x⦌𝑋 ∈ B ∧ ⦋z / x⦌𝑋 ∈ B))
44		potr 4036	. . . . 5 ⊢ ((𝑅 Po B ∧ (⦋v / x⦌𝑋 ∈ B ∧ ⦋w / x⦌𝑋 ∈ B ∧ ⦋z / x⦌𝑋 ∈ B)) → ((⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋 ∧ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋) → ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋))
45		df-br 3756	. . . . . . 7 ⊢ (v𝑆w ↔ ⟨v, w⟩ ∈ 𝑆)
46	9	eleq2i 2101	. . . . . . 7 ⊢ (⟨v, w⟩ ∈ 𝑆 ↔ ⟨v, w⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌})
47		nfv 1418	. . . . . . . 8 ⊢ Ⅎy⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋
48		vex 2554	. . . . . . . 8 ⊢ w ∈ V
49		csbeq1 2849	. . . . . . . . . 10 ⊢ (y = w → ⦋y / x⦌𝑋 = ⦋w / x⦌𝑋)
50	19, 49	syl5eqr 2083	. . . . . . . . 9 ⊢ (y = w → 𝑌 = ⦋w / x⦌𝑋)
51	50	breq2d 3767	. . . . . . . 8 ⊢ (y = w → (⦋v / x⦌𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋))
52	13, 47, 15, 48, 16, 51	opelopabf 4002	. . . . . . 7 ⊢ (⟨v, w⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋)
53	45, 46, 52	3bitri 195	. . . . . 6 ⊢ (v𝑆w ↔ ⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋)
54		df-br 3756	. . . . . . 7 ⊢ (w𝑆z ↔ ⟨w, z⟩ ∈ 𝑆)
55	9	eleq2i 2101	. . . . . . 7 ⊢ (⟨w, z⟩ ∈ 𝑆 ↔ ⟨w, z⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌})
56	29, 11, 12	nfbr 3799	. . . . . . . 8 ⊢ Ⅎx⦋w / x⦌𝑋𝑅𝑌
57		nfv 1418	. . . . . . . 8 ⊢ Ⅎy⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋
58		vex 2554	. . . . . . . 8 ⊢ z ∈ V
59	31	breq1d 3765	. . . . . . . 8 ⊢ (x = w → (𝑋𝑅𝑌 ↔ ⦋w / x⦌𝑋𝑅𝑌))
60		csbeq1 2849	. . . . . . . . . 10 ⊢ (y = z → ⦋y / x⦌𝑋 = ⦋z / x⦌𝑋)
61	19, 60	syl5eqr 2083	. . . . . . . . 9 ⊢ (y = z → 𝑌 = ⦋z / x⦌𝑋)
62	61	breq2d 3767	. . . . . . . 8 ⊢ (y = z → (⦋w / x⦌𝑋𝑅𝑌 ↔ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋))
63	56, 57, 48, 58, 59, 62	opelopabf 4002	. . . . . . 7 ⊢ (⟨w, z⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋)
64	54, 55, 63	3bitri 195	. . . . . 6 ⊢ (w𝑆z ↔ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋)
65	53, 64	anbi12i 433	. . . . 5 ⊢ ((v𝑆w ∧ w𝑆z) ↔ (⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋 ∧ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋))
66		df-br 3756	. . . . . 6 ⊢ (v𝑆z ↔ ⟨v, z⟩ ∈ 𝑆)
67	9	eleq2i 2101	. . . . . 6 ⊢ (⟨v, z⟩ ∈ 𝑆 ↔ ⟨v, z⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌})
68		nfv 1418	. . . . . . 7 ⊢ Ⅎy⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋
69	61	breq2d 3767	. . . . . . 7 ⊢ (y = z → (⦋v / x⦌𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋))
70	13, 68, 15, 58, 16, 69	opelopabf 4002	. . . . . 6 ⊢ (⟨v, z⟩ ∈ {⟨x, y⟩ ∣ 𝑋𝑅𝑌} ↔ ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋)
71	66, 67, 70	3bitri 195	. . . . 5 ⊢ (v𝑆z ↔ ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋)
72	44, 65, 71	3imtr4g 194	. . . 4 ⊢ ((𝑅 Po B ∧ (⦋v / x⦌𝑋 ∈ B ∧ ⦋w / x⦌𝑋 ∈ B ∧ ⦋z / x⦌𝑋 ∈ B)) → ((v𝑆w ∧ w𝑆z) → v𝑆z))
73	72	adantlr 446	. . 3 ⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ (⦋v / x⦌𝑋 ∈ B ∧ ⦋w / x⦌𝑋 ∈ B ∧ ⦋z / x⦌𝑋 ∈ B)) → ((v𝑆w ∧ w𝑆z) → v𝑆z))
74	43, 73	syldan 266	. 2 ⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ (v ∈ A ∧ w ∈ A ∧ z ∈ A)) → ((v𝑆w ∧ w𝑆z) → v𝑆z))
75	27, 74	ispod 4032	1 ⊢ ((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) → 𝑆 Po A)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∀wral 2300  ⦋csb 2846  ⟨cop 3370   class class class wbr 3755  {copab 3808   Po wpo 4022

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-po 4024

This theorem is referenced by: (None)