Step |
Hyp |
Ref |
Expression |
1 |
|
wemapso.t |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } |
2 |
|
wemaplem2.p |
⊢ ( 𝜑 → 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) ) |
3 |
|
wemaplem2.x |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) ) |
4 |
|
wemaplem2.q |
⊢ ( 𝜑 → 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) ) |
5 |
|
wemaplem2.r |
⊢ ( 𝜑 → 𝑅 Or 𝐴 ) |
6 |
|
wemaplem2.s |
⊢ ( 𝜑 → 𝑆 Po 𝐵 ) |
7 |
|
wemaplem2.px1 |
⊢ ( 𝜑 → 𝑎 ∈ 𝐴 ) |
8 |
|
wemaplem2.px2 |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ) |
9 |
|
wemaplem2.px3 |
⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ) |
10 |
|
wemaplem2.xq1 |
⊢ ( 𝜑 → 𝑏 ∈ 𝐴 ) |
11 |
|
wemaplem2.xq2 |
⊢ ( 𝜑 → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) |
12 |
|
wemaplem2.xq3 |
⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) |
13 |
7 10
|
ifcld |
⊢ ( 𝜑 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ∈ 𝐴 ) |
14 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ) |
15 |
|
breq1 |
⊢ ( 𝑐 = 𝑎 → ( 𝑐 𝑅 𝑏 ↔ 𝑎 𝑅 𝑏 ) ) |
16 |
|
fveq2 |
⊢ ( 𝑐 = 𝑎 → ( 𝑋 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑎 ) ) |
17 |
|
fveq2 |
⊢ ( 𝑐 = 𝑎 → ( 𝑄 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑎 ) ) |
18 |
16 17
|
eqeq12d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ↔ ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) ) |
19 |
15 18
|
imbi12d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ↔ ( 𝑎 𝑅 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) ) ) |
20 |
19 12 7
|
rspcdva |
⊢ ( 𝜑 → ( 𝑎 𝑅 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) ) |
21 |
20
|
imp |
⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑋 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑎 ) ) |
22 |
14 21
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ) |
23 |
|
iftrue |
⊢ ( 𝑎 𝑅 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = 𝑎 ) |
24 |
23
|
fveq2d |
⊢ ( 𝑎 𝑅 𝑏 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑃 ‘ 𝑎 ) ) |
25 |
23
|
fveq2d |
⊢ ( 𝑎 𝑅 𝑏 → ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑄 ‘ 𝑎 ) ) |
26 |
24 25
|
breq12d |
⊢ ( 𝑎 𝑅 𝑏 → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ) ) |
27 |
26
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ) ) |
28 |
22 27
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑎 𝑅 𝑏 ) → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
29 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → 𝑆 Po 𝐵 ) |
30 |
|
elmapi |
⊢ ( 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑃 : 𝐴 ⟶ 𝐵 ) |
31 |
2 30
|
syl |
⊢ ( 𝜑 → 𝑃 : 𝐴 ⟶ 𝐵 ) |
32 |
31 10
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ) |
33 |
|
elmapi |
⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑋 : 𝐴 ⟶ 𝐵 ) |
34 |
3 33
|
syl |
⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐵 ) |
35 |
34 10
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ) |
36 |
|
elmapi |
⊢ ( 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑄 : 𝐴 ⟶ 𝐵 ) |
37 |
4 36
|
syl |
⊢ ( 𝜑 → 𝑄 : 𝐴 ⟶ 𝐵 ) |
38 |
37 10
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) |
39 |
32 35 38
|
3jca |
⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) ) |
40 |
39
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) ) |
41 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) ) |
42 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝑋 ‘ 𝑎 ) = ( 𝑋 ‘ 𝑏 ) ) |
43 |
41 42
|
breq12d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑋 ‘ 𝑎 ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ) ) |
44 |
8 43
|
syl5ibcom |
⊢ ( 𝜑 → ( 𝑎 = 𝑏 → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ) ) |
45 |
44
|
imp |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ) |
46 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) |
47 |
|
potr |
⊢ ( ( 𝑆 Po 𝐵 ∧ ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) ) → ( ( ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ∧ ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) |
48 |
47
|
imp |
⊢ ( ( ( 𝑆 Po 𝐵 ∧ ( ( 𝑃 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝑄 ‘ 𝑏 ) ∈ 𝐵 ) ) ∧ ( ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑋 ‘ 𝑏 ) ∧ ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) |
49 |
29 40 45 46 48
|
syl22anc |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) |
50 |
|
ifeq1 |
⊢ ( 𝑎 = 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑏 ) ) |
51 |
|
ifid |
⊢ if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑏 ) = 𝑏 |
52 |
50 51
|
eqtrdi |
⊢ ( 𝑎 = 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = 𝑏 ) |
53 |
52
|
fveq2d |
⊢ ( 𝑎 = 𝑏 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑃 ‘ 𝑏 ) ) |
54 |
52
|
fveq2d |
⊢ ( 𝑎 = 𝑏 → ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑄 ‘ 𝑏 ) ) |
55 |
53 54
|
breq12d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) |
56 |
55
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) |
57 |
49 56
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑎 = 𝑏 ) → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
58 |
|
breq1 |
⊢ ( 𝑐 = 𝑏 → ( 𝑐 𝑅 𝑎 ↔ 𝑏 𝑅 𝑎 ) ) |
59 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝑃 ‘ 𝑐 ) = ( 𝑃 ‘ 𝑏 ) ) |
60 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑏 ) ) |
61 |
59 60
|
eqeq12d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ↔ ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) ) |
62 |
58 61
|
imbi12d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ↔ ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) ) ) |
63 |
62 9 10
|
rspcdva |
⊢ ( 𝜑 → ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) ) |
64 |
63
|
imp |
⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑃 ‘ 𝑏 ) = ( 𝑋 ‘ 𝑏 ) ) |
65 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑋 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) |
66 |
64 65
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) |
67 |
|
sopo |
⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 ) |
68 |
5 67
|
syl |
⊢ ( 𝜑 → 𝑅 Po 𝐴 ) |
69 |
|
po2nr |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ) → ¬ ( 𝑏 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) ) |
70 |
68 10 7 69
|
syl12anc |
⊢ ( 𝜑 → ¬ ( 𝑏 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) ) |
71 |
|
nan |
⊢ ( ( 𝜑 → ¬ ( 𝑏 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) ) ↔ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) |
72 |
70 71
|
mpbi |
⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) |
73 |
|
iffalse |
⊢ ( ¬ 𝑎 𝑅 𝑏 → if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) = 𝑏 ) |
74 |
73
|
fveq2d |
⊢ ( ¬ 𝑎 𝑅 𝑏 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑃 ‘ 𝑏 ) ) |
75 |
73
|
fveq2d |
⊢ ( ¬ 𝑎 𝑅 𝑏 → ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) = ( 𝑄 ‘ 𝑏 ) ) |
76 |
74 75
|
breq12d |
⊢ ( ¬ 𝑎 𝑅 𝑏 → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) |
77 |
72 76
|
syl |
⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ↔ ( 𝑃 ‘ 𝑏 ) 𝑆 ( 𝑄 ‘ 𝑏 ) ) ) |
78 |
66 77
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑏 𝑅 𝑎 ) → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
79 |
|
solin |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) ) |
80 |
5 7 10 79
|
syl12anc |
⊢ ( 𝜑 → ( 𝑎 𝑅 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) ) |
81 |
28 57 78 80
|
mpjao3dan |
⊢ ( 𝜑 → ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
82 |
|
r19.26 |
⊢ ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ↔ ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
83 |
9 12 82
|
sylanbrc |
⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
84 |
5 7 10
|
3jca |
⊢ ( 𝜑 → ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) |
85 |
|
anim12 |
⊢ ( ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ∧ ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
86 |
|
eqtr |
⊢ ( ( ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ∧ ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) |
87 |
85 86
|
syl6 |
⊢ ( ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) |
88 |
87
|
ralimi |
⊢ ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) |
89 |
|
simpl1 |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑅 Or 𝐴 ) |
90 |
|
simpr |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ 𝐴 ) |
91 |
|
simpl2 |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 ) |
92 |
|
simpl3 |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑏 ∈ 𝐴 ) |
93 |
|
soltmin |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ↔ ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) ) ) |
94 |
89 90 91 92 93
|
syl13anc |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ↔ ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) ) ) |
95 |
94
|
biimpd |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) ) ) |
96 |
95
|
imim1d |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑐 ∈ 𝐴 ) → ( ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) → ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
97 |
96
|
ralimdva |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 ∧ 𝑐 𝑅 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
98 |
84 88 97
|
syl2im |
⊢ ( 𝜑 → ( ∀ 𝑐 ∈ 𝐴 ( ( 𝑐 𝑅 𝑎 → ( 𝑃 ‘ 𝑐 ) = ( 𝑋 ‘ 𝑐 ) ) ∧ ( 𝑐 𝑅 𝑏 → ( 𝑋 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
99 |
83 98
|
mpd |
⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) |
100 |
|
fveq2 |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑑 ) = ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
101 |
|
fveq2 |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑄 ‘ 𝑑 ) = ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
102 |
100 101
|
breq12d |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ↔ ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) ) |
103 |
|
breq2 |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑐 𝑅 𝑑 ↔ 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ) |
104 |
103
|
imbi1d |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ↔ ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
105 |
104
|
ralbidv |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
106 |
102 105
|
anbi12d |
⊢ ( 𝑑 = if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ↔ ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) |
107 |
106
|
rspcev |
⊢ ( ( if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ∈ 𝐴 ∧ ( ( 𝑃 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) 𝑆 ( 𝑄 ‘ if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑎 , 𝑏 ) → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) → ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
108 |
13 81 99 107
|
syl12anc |
⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) |
109 |
1
|
wemaplem1 |
⊢ ( ( 𝑃 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑄 ∈ ( 𝐵 ↑m 𝐴 ) ) → ( 𝑃 𝑇 𝑄 ↔ ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) |
110 |
2 4 109
|
syl2anc |
⊢ ( 𝜑 → ( 𝑃 𝑇 𝑄 ↔ ∃ 𝑑 ∈ 𝐴 ( ( 𝑃 ‘ 𝑑 ) 𝑆 ( 𝑄 ‘ 𝑑 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑑 → ( 𝑃 ‘ 𝑐 ) = ( 𝑄 ‘ 𝑐 ) ) ) ) ) |
111 |
108 110
|
mpbird |
⊢ ( 𝜑 → 𝑃 𝑇 𝑄 ) |