wemaplem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wemaplem2		Structured version Visualization version GIF version

Theorem wemaplem2 8335

Description: Lemma for wemapso 8339. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.)

**Hypotheses**
Ref	Expression
wemapso.t	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
wemaplem2.a	⊢ (𝜑 → 𝐴 ∈ V)
wemaplem2.p	⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑_𝑚 𝐴))
wemaplem2.x	⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑_𝑚 𝐴))
wemaplem2.q	⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑_𝑚 𝐴))
wemaplem2.r	⊢ (𝜑 → 𝑅 Or 𝐴)
wemaplem2.s	⊢ (𝜑 → 𝑆 Po 𝐵)
wemaplem2.px1	⊢ (𝜑 → 𝑎 ∈ 𝐴)
wemaplem2.px2	⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎))
wemaplem2.px3	⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)))
wemaplem2.xq1	⊢ (𝜑 → 𝑏 ∈ 𝐴)
wemaplem2.xq2	⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏))
wemaplem2.xq3	⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)))

**Assertion**
Ref	Expression
wemaplem2	⊢ (𝜑 → 𝑃𝑇𝑄)

Distinct variable groups: 𝑎,𝑏,𝑐,𝑥,𝐵 𝑇,𝑎,𝑏,𝑐 𝑤,𝑎,𝑦,𝑧,𝑋,𝑏,𝑐,𝑥 𝐴,𝑎,𝑏,𝑐,𝑤,𝑥,𝑦,𝑧 𝑃,𝑎,𝑏,𝑐,𝑤,𝑥,𝑦,𝑧 𝑄,𝑎,𝑏,𝑐,𝑤,𝑥,𝑦,𝑧 𝑅,𝑎,𝑏,𝑐,𝑤,𝑥,𝑦,𝑧 𝑆,𝑎,𝑏,𝑐,𝑤,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑧,𝑤,𝑎,𝑏,𝑐) 𝐵(𝑦,𝑧,𝑤) 𝑇(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem wemaplem2 Dummy variable 𝑑 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wemaplem2.px1	. . . 4 ⊢ (𝜑 → 𝑎 ∈ 𝐴)
2		wemaplem2.xq1	. . . 4 ⊢ (𝜑 → 𝑏 ∈ 𝐴)
3	1, 2	ifcld 4081	. . 3 ⊢ (𝜑 → if(𝑎𝑅𝑏, 𝑎, 𝑏) ∈ 𝐴)
4		wemaplem2.px2	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎))
5	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎𝑅𝑏) → (𝑃‘𝑎)𝑆(𝑋‘𝑎))
6		wemaplem2.xq3	. . . . . . . 8 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)))
7		breq1 4586	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → (𝑐𝑅𝑏 ↔ 𝑎𝑅𝑏))
8		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑎 → (𝑋‘𝑐) = (𝑋‘𝑎))
9		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑎 → (𝑄‘𝑐) = (𝑄‘𝑎))
10	8, 9	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → ((𝑋‘𝑐) = (𝑄‘𝑐) ↔ (𝑋‘𝑎) = (𝑄‘𝑎)))
11	7, 10	imbi12d 333	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → ((𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)) ↔ (𝑎𝑅𝑏 → (𝑋‘𝑎) = (𝑄‘𝑎))))
12	11	rspcva 3280	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐴 ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) → (𝑎𝑅𝑏 → (𝑋‘𝑎) = (𝑄‘𝑎)))
13	1, 6, 12	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (𝑎𝑅𝑏 → (𝑋‘𝑎) = (𝑄‘𝑎)))
14	13	imp 444	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎𝑅𝑏) → (𝑋‘𝑎) = (𝑄‘𝑎))
15	5, 14	breqtrd 4609	. . . . 5 ⊢ ((𝜑 ∧ 𝑎𝑅𝑏) → (𝑃‘𝑎)𝑆(𝑄‘𝑎))
16		iftrue 4042	. . . . . . . 8 ⊢ (𝑎𝑅𝑏 → if(𝑎𝑅𝑏, 𝑎, 𝑏) = 𝑎)
17	16	fveq2d 6107	. . . . . . 7 ⊢ (𝑎𝑅𝑏 → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) = (𝑃‘𝑎))
18	16	fveq2d 6107	. . . . . . 7 ⊢ (𝑎𝑅𝑏 → (𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) = (𝑄‘𝑎))
19	17, 18	breq12d 4596	. . . . . 6 ⊢ (𝑎𝑅𝑏 → ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ↔ (𝑃‘𝑎)𝑆(𝑄‘𝑎)))
20	19	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎𝑅𝑏) → ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ↔ (𝑃‘𝑎)𝑆(𝑄‘𝑎)))
21	15, 20	mpbird 246	. . . 4 ⊢ ((𝜑 ∧ 𝑎𝑅𝑏) → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)))
22		wemaplem2.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 Po 𝐵)
23	22	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → 𝑆 Po 𝐵)
24		wemaplem2.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑_𝑚 𝐴))
25		elmapi 7765	. . . . . . . . . 10 ⊢ (𝑃 ∈ (𝐵 ↑_𝑚 𝐴) → 𝑃:𝐴⟶𝐵)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑃:𝐴⟶𝐵)
27	26, 2	ffvelrnd 6268	. . . . . . . 8 ⊢ (𝜑 → (𝑃‘𝑏) ∈ 𝐵)
28		wemaplem2.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑_𝑚 𝐴))
29		elmapi 7765	. . . . . . . . . 10 ⊢ (𝑋 ∈ (𝐵 ↑_𝑚 𝐴) → 𝑋:𝐴⟶𝐵)
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋:𝐴⟶𝐵)
31	30, 2	ffvelrnd 6268	. . . . . . . 8 ⊢ (𝜑 → (𝑋‘𝑏) ∈ 𝐵)
32		wemaplem2.q	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑_𝑚 𝐴))
33		elmapi 7765	. . . . . . . . . 10 ⊢ (𝑄 ∈ (𝐵 ↑_𝑚 𝐴) → 𝑄:𝐴⟶𝐵)
34	32, 33	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:𝐴⟶𝐵)
35	34, 2	ffvelrnd 6268	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑏) ∈ 𝐵)
36	27, 31, 35	3jca 1235	. . . . . . 7 ⊢ (𝜑 → ((𝑃‘𝑏) ∈ 𝐵 ∧ (𝑋‘𝑏) ∈ 𝐵 ∧ (𝑄‘𝑏) ∈ 𝐵))
37	36	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → ((𝑃‘𝑏) ∈ 𝐵 ∧ (𝑋‘𝑏) ∈ 𝐵 ∧ (𝑄‘𝑏) ∈ 𝐵))
38		fveq2 6103	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (𝑃‘𝑎) = (𝑃‘𝑏))
39		fveq2 6103	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (𝑋‘𝑎) = (𝑋‘𝑏))
40	38, 39	breq12d 4596	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ((𝑃‘𝑎)𝑆(𝑋‘𝑎) ↔ (𝑃‘𝑏)𝑆(𝑋‘𝑏)))
41	4, 40	syl5ibcom 234	. . . . . . 7 ⊢ (𝜑 → (𝑎 = 𝑏 → (𝑃‘𝑏)𝑆(𝑋‘𝑏)))
42	41	imp 444	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → (𝑃‘𝑏)𝑆(𝑋‘𝑏))
43		wemaplem2.xq2	. . . . . . 7 ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏))
44	43	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → (𝑋‘𝑏)𝑆(𝑄‘𝑏))
45		potr 4971	. . . . . . 7 ⊢ ((𝑆 Po 𝐵 ∧ ((𝑃‘𝑏) ∈ 𝐵 ∧ (𝑋‘𝑏) ∈ 𝐵 ∧ (𝑄‘𝑏) ∈ 𝐵)) → (((𝑃‘𝑏)𝑆(𝑋‘𝑏) ∧ (𝑋‘𝑏)𝑆(𝑄‘𝑏)) → (𝑃‘𝑏)𝑆(𝑄‘𝑏)))
46	45	imp 444	. . . . . 6 ⊢ (((𝑆 Po 𝐵 ∧ ((𝑃‘𝑏) ∈ 𝐵 ∧ (𝑋‘𝑏) ∈ 𝐵 ∧ (𝑄‘𝑏) ∈ 𝐵)) ∧ ((𝑃‘𝑏)𝑆(𝑋‘𝑏) ∧ (𝑋‘𝑏)𝑆(𝑄‘𝑏))) → (𝑃‘𝑏)𝑆(𝑄‘𝑏))
47	23, 37, 42, 44, 46	syl22anc 1319	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → (𝑃‘𝑏)𝑆(𝑄‘𝑏))
48		ifeq1 4040	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → if(𝑎𝑅𝑏, 𝑎, 𝑏) = if(𝑎𝑅𝑏, 𝑏, 𝑏))
49		ifid 4075	. . . . . . . . 9 ⊢ if(𝑎𝑅𝑏, 𝑏, 𝑏) = 𝑏
50	48, 49	syl6eq 2660	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → if(𝑎𝑅𝑏, 𝑎, 𝑏) = 𝑏)
51	50	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) = (𝑃‘𝑏))
52	50	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) = (𝑄‘𝑏))
53	51, 52	breq12d 4596	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ↔ (𝑃‘𝑏)𝑆(𝑄‘𝑏)))
54	53	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ↔ (𝑃‘𝑏)𝑆(𝑄‘𝑏)))
55	47, 54	mpbird 246	. . . 4 ⊢ ((𝜑 ∧ 𝑎 = 𝑏) → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)))
56		wemaplem2.px3	. . . . . . . 8 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)))
57		breq1 4586	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → (𝑐𝑅𝑎 ↔ 𝑏𝑅𝑎))
58		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑏 → (𝑃‘𝑐) = (𝑃‘𝑏))
59		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑏 → (𝑋‘𝑐) = (𝑋‘𝑏))
60	58, 59	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → ((𝑃‘𝑐) = (𝑋‘𝑐) ↔ (𝑃‘𝑏) = (𝑋‘𝑏)))
61	57, 60	imbi12d 333	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → ((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ↔ (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑋‘𝑏))))
62	61	rspcva 3280	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝐴 ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐))) → (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑋‘𝑏)))
63	2, 56, 62	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑋‘𝑏)))
64	63	imp 444	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏𝑅𝑎) → (𝑃‘𝑏) = (𝑋‘𝑏))
65	43	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏𝑅𝑎) → (𝑋‘𝑏)𝑆(𝑄‘𝑏))
66	64, 65	eqbrtrd 4605	. . . . 5 ⊢ ((𝜑 ∧ 𝑏𝑅𝑎) → (𝑃‘𝑏)𝑆(𝑄‘𝑏))
67		wemaplem2.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 Or 𝐴)
68		sopo 4976	. . . . . . . . 9 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
69	67, 68	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑅 Po 𝐴)
70		po2nr 4972	. . . . . . . 8 ⊢ ((𝑅 Po 𝐴 ∧ (𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴)) → ¬ (𝑏𝑅𝑎 ∧ 𝑎𝑅𝑏))
71	69, 2, 1, 70	syl12anc 1316	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑏𝑅𝑎 ∧ 𝑎𝑅𝑏))
72		nan 602	. . . . . . 7 ⊢ ((𝜑 → ¬ (𝑏𝑅𝑎 ∧ 𝑎𝑅𝑏)) ↔ ((𝜑 ∧ 𝑏𝑅𝑎) → ¬ 𝑎𝑅𝑏))
73	71, 72	mpbi 219	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏𝑅𝑎) → ¬ 𝑎𝑅𝑏)
74		iffalse 4045	. . . . . . . 8 ⊢ (¬ 𝑎𝑅𝑏 → if(𝑎𝑅𝑏, 𝑎, 𝑏) = 𝑏)
75	74	fveq2d 6107	. . . . . . 7 ⊢ (¬ 𝑎𝑅𝑏 → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) = (𝑃‘𝑏))
76	74	fveq2d 6107	. . . . . . 7 ⊢ (¬ 𝑎𝑅𝑏 → (𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) = (𝑄‘𝑏))
77	75, 76	breq12d 4596	. . . . . 6 ⊢ (¬ 𝑎𝑅𝑏 → ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ↔ (𝑃‘𝑏)𝑆(𝑄‘𝑏)))
78	73, 77	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑏𝑅𝑎) → ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ↔ (𝑃‘𝑏)𝑆(𝑄‘𝑏)))
79	66, 78	mpbird 246	. . . 4 ⊢ ((𝜑 ∧ 𝑏𝑅𝑎) → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)))
80		solin 4982	. . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎))
81	67, 1, 2, 80	syl12anc 1316	. . . 4 ⊢ (𝜑 → (𝑎𝑅𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑅𝑎))
82	21, 55, 79, 81	mpjao3dan 1387	. . 3 ⊢ (𝜑 → (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)))
83		r19.26 3046	. . . . 5 ⊢ (∀𝑐 ∈ 𝐴 ((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) ↔ (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))))
84	56, 6, 83	sylanbrc 695	. . . 4 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))))
85	67, 1, 2	3jca 1235	. . . . 5 ⊢ (𝜑 → (𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))
86		prth 593	. . . . . . 7 ⊢ (((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) → ((𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏) → ((𝑃‘𝑐) = (𝑋‘𝑐) ∧ (𝑋‘𝑐) = (𝑄‘𝑐))))
87		eqtr 2629	. . . . . . 7 ⊢ (((𝑃‘𝑐) = (𝑋‘𝑐) ∧ (𝑋‘𝑐) = (𝑄‘𝑐)) → (𝑃‘𝑐) = (𝑄‘𝑐))
88	86, 87	syl6 34	. . . . . 6 ⊢ (((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) → ((𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)))
89	88	ralimi 2936	. . . . 5 ⊢ (∀𝑐 ∈ 𝐴 ((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) → ∀𝑐 ∈ 𝐴 ((𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)))
90		simpl1 1057	. . . . . . . . 9 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → 𝑅 Or 𝐴)
91		simpr 476	. . . . . . . . 9 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴)
92		simpl2 1058	. . . . . . . . 9 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → 𝑎 ∈ 𝐴)
93		simpl3 1059	. . . . . . . . 9 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → 𝑏 ∈ 𝐴)
94		soltmin 5451	. . . . . . . . 9 ⊢ ((𝑅 Or 𝐴 ∧ (𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) ↔ (𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏)))
95	90, 91, 92, 93, 94	syl13anc 1320	. . . . . . . 8 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) ↔ (𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏)))
96	95	biimpd 218	. . . . . . 7 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏)))
97	96	imim1d 80	. . . . . 6 ⊢ (((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ 𝐴) → (((𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)) → (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐))))
98	97	ralimdva 2945	. . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ 𝐴 ((𝑐𝑅𝑎 ∧ 𝑐𝑅𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)) → ∀𝑐 ∈ 𝐴 (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐))))
99	85, 89, 98	syl2im 39	. . . 4 ⊢ (𝜑 → (∀𝑐 ∈ 𝐴 ((𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)) ∧ (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) → ∀𝑐 ∈ 𝐴 (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐))))
100	84, 99	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)))
101		fveq2 6103	. . . . . 6 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑑) = (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏)))
102		fveq2 6103	. . . . . 6 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑄‘𝑑) = (𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)))
103	101, 102	breq12d 4596	. . . . 5 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → ((𝑃‘𝑑)𝑆(𝑄‘𝑑) ↔ (𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏))))
104		breq2 4587	. . . . . . 7 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑐𝑅𝑑 ↔ 𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏)))
105	104	imbi1d 330	. . . . . 6 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → ((𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐)) ↔ (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐))))
106	105	ralbidv 2969	. . . . 5 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐)) ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐))))
107	103, 106	anbi12d 743	. . . 4 ⊢ (𝑑 = if(𝑎𝑅𝑏, 𝑎, 𝑏) → (((𝑃‘𝑑)𝑆(𝑄‘𝑑) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐))) ↔ ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)))))
108	107	rspcev 3282	. . 3 ⊢ ((if(𝑎𝑅𝑏, 𝑎, 𝑏) ∈ 𝐴 ∧ ((𝑃‘if(𝑎𝑅𝑏, 𝑎, 𝑏))𝑆(𝑄‘if(𝑎𝑅𝑏, 𝑎, 𝑏)) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅if(𝑎𝑅𝑏, 𝑎, 𝑏) → (𝑃‘𝑐) = (𝑄‘𝑐)))) → ∃𝑑 ∈ 𝐴 ((𝑃‘𝑑)𝑆(𝑄‘𝑑) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐))))
109	3, 82, 100, 108	syl12anc 1316	. 2 ⊢ (𝜑 → ∃𝑑 ∈ 𝐴 ((𝑃‘𝑑)𝑆(𝑄‘𝑑) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐))))
110		wemapso.t	. . . 4 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
111	110	wemaplem1 8334	. . 3 ⊢ ((𝑃 ∈ (𝐵 ↑_𝑚 𝐴) ∧ 𝑄 ∈ (𝐵 ↑_𝑚 𝐴)) → (𝑃𝑇𝑄 ↔ ∃𝑑 ∈ 𝐴 ((𝑃‘𝑑)𝑆(𝑄‘𝑑) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐)))))
112	24, 32, 111	syl2anc 691	. 2 ⊢ (𝜑 → (𝑃𝑇𝑄 ↔ ∃𝑑 ∈ 𝐴 ((𝑃‘𝑑)𝑆(𝑄‘𝑑) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑑 → (𝑃‘𝑐) = (𝑄‘𝑐)))))
113	109, 112	mpbird 246	1 ⊢ (𝜑 → 𝑃𝑇𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∨ w3o 1030 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ifcif 4036 class class class wbr 4583 {copab 4642 Po wpo 4957 Or wor 4958 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↑_𝑚 cmap 7744

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-8 1979 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-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 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-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-po 4959 df-so 4960 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-1st 7059 df-2nd 7060 df-map 7746

This theorem is referenced by: wemaplem3 8336

W3C validator