Step |
Hyp |
Ref |
Expression |
1 |
|
isoun.1 |
⊢ ( 𝜑 → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) |
2 |
|
isoun.2 |
⊢ ( 𝜑 → 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ) |
3 |
|
isoun.3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) → 𝑥 𝑅 𝑦 ) |
4 |
|
isoun.4 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) → 𝑧 𝑆 𝑤 ) |
5 |
|
isoun.5 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) → ¬ 𝑥 𝑅 𝑦 ) |
6 |
|
isoun.6 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵 ) → ¬ 𝑧 𝑆 𝑤 ) |
7 |
|
isoun.7 |
⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) = ∅ ) |
8 |
|
isoun.8 |
⊢ ( 𝜑 → ( 𝐵 ∩ 𝐷 ) = ∅ ) |
9 |
|
isof1o |
⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 ) |
10 |
1 9
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝐴 –1-1-onto→ 𝐵 ) |
11 |
|
isof1o |
⊢ ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) → 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) |
12 |
2 11
|
syl |
⊢ ( 𝜑 → 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) |
13 |
|
f1oun |
⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐻 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) ) |
14 |
10 12 7 8 13
|
syl22anc |
⊢ ( 𝜑 → ( 𝐻 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) ) |
15 |
|
elun |
⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) ) |
16 |
|
elun |
⊢ ( 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐶 ) ) |
17 |
|
isorel |
⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
18 |
1 17
|
sylan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
19 |
|
f1ofn |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Fn 𝐴 ) |
20 |
10 19
|
syl |
⊢ ( 𝜑 → 𝐻 Fn 𝐴 ) |
21 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 Fn 𝐴 ) |
22 |
|
f1ofn |
⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 Fn 𝐶 ) |
23 |
12 22
|
syl |
⊢ ( 𝜑 → 𝐺 Fn 𝐶 ) |
24 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐺 Fn 𝐶 ) |
25 |
7
|
anim1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑥 ∈ 𝐴 ) ) |
26 |
|
fvun1 |
⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) |
27 |
21 24 25 26
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) |
28 |
27
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) |
29 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐻 Fn 𝐴 ) |
30 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐺 Fn 𝐶 ) |
31 |
7
|
anim1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑦 ∈ 𝐴 ) ) |
32 |
|
fvun1 |
⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) ) |
33 |
29 30 31 32
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) ) |
34 |
33
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) ) |
35 |
28 34
|
breq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
36 |
18 35
|
bitr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
37 |
36
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
38 |
3
|
3expb |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 𝑅 𝑦 ) |
39 |
4
|
3expia |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑤 ∈ 𝐷 → 𝑧 𝑆 𝑤 ) ) |
40 |
39
|
ralrimiv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ∀ 𝑤 ∈ 𝐷 𝑧 𝑆 𝑤 ) |
41 |
40
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐷 𝑧 𝑆 𝑤 ) |
42 |
41
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐷 𝑧 𝑆 𝑤 ) |
43 |
|
f1of |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 ) |
44 |
10 43
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 ) |
45 |
44
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ) |
46 |
45
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ) |
47 |
|
f1of |
⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 : 𝐶 ⟶ 𝐷 ) |
48 |
12 47
|
syl |
⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 ) |
49 |
48
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐷 ) |
50 |
49
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐷 ) |
51 |
|
breq1 |
⊢ ( 𝑧 = ( 𝐻 ‘ 𝑥 ) → ( 𝑧 𝑆 𝑤 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 𝑤 ) ) |
52 |
|
breq2 |
⊢ ( 𝑤 = ( 𝐺 ‘ 𝑦 ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 𝑤 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) ) |
53 |
51 52
|
rspc2v |
⊢ ( ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝐷 ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐷 𝑧 𝑆 𝑤 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) ) |
54 |
46 50 53
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐷 𝑧 𝑆 𝑤 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) ) |
55 |
42 54
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) |
56 |
27
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) |
57 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐻 Fn 𝐴 ) |
58 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐺 Fn 𝐶 ) |
59 |
7
|
anim1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑦 ∈ 𝐶 ) ) |
60 |
|
fvun2 |
⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
61 |
57 58 59 60
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
62 |
61
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
63 |
55 56 62
|
3brtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) |
64 |
38 63
|
2thd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
65 |
64
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
66 |
37 65
|
jaodan |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
67 |
16 66
|
sylan2b |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
68 |
67
|
ex |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) ) |
69 |
5
|
3expb |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ¬ 𝑥 𝑅 𝑦 ) |
70 |
6
|
3expia |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝑤 ∈ 𝐵 → ¬ 𝑧 𝑆 𝑤 ) ) |
71 |
70
|
ralrimiv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ∀ 𝑤 ∈ 𝐵 ¬ 𝑧 𝑆 𝑤 ) |
72 |
71
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐷 ∀ 𝑤 ∈ 𝐵 ¬ 𝑧 𝑆 𝑤 ) |
73 |
72
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ∀ 𝑧 ∈ 𝐷 ∀ 𝑤 ∈ 𝐵 ¬ 𝑧 𝑆 𝑤 ) |
74 |
48
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐷 ) |
75 |
74
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐷 ) |
76 |
44
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) |
77 |
76
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) |
78 |
|
breq1 |
⊢ ( 𝑧 = ( 𝐺 ‘ 𝑥 ) → ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑥 ) 𝑆 𝑤 ) ) |
79 |
78
|
notbid |
⊢ ( 𝑧 = ( 𝐺 ‘ 𝑥 ) → ( ¬ 𝑧 𝑆 𝑤 ↔ ¬ ( 𝐺 ‘ 𝑥 ) 𝑆 𝑤 ) ) |
80 |
|
breq2 |
⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
81 |
80
|
notbid |
⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( ¬ ( 𝐺 ‘ 𝑥 ) 𝑆 𝑤 ↔ ¬ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
82 |
79 81
|
rspc2v |
⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐷 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐷 ∀ 𝑤 ∈ 𝐵 ¬ 𝑧 𝑆 𝑤 → ¬ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
83 |
75 77 82
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∀ 𝑧 ∈ 𝐷 ∀ 𝑤 ∈ 𝐵 ¬ 𝑧 𝑆 𝑤 → ¬ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
84 |
73 83
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ¬ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) |
85 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐻 Fn 𝐴 ) |
86 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐺 Fn 𝐶 ) |
87 |
7
|
anim1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑥 ∈ 𝐶 ) ) |
88 |
|
fvun2 |
⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ 𝑥 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
89 |
85 86 87 88
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
90 |
89
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
91 |
33
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) ) |
92 |
90 91
|
breq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) |
93 |
84 92
|
mtbird |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ¬ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) |
94 |
69 93
|
2falsed |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
95 |
94
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
96 |
|
isorel |
⊢ ( ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) ) |
97 |
2 96
|
sylan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) ) |
98 |
89
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
99 |
61
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
100 |
98 99
|
breq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) 𝑆 ( 𝐺 ‘ 𝑦 ) ) ) |
101 |
97 100
|
bitr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
102 |
101
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
103 |
95 102
|
jaodan |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
104 |
16 103
|
sylan2b |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
105 |
104
|
ex |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) ) |
106 |
68 105
|
jaodan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) ) → ( 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) ) |
107 |
15 106
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ) → ( 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) ) |
108 |
107
|
ralrimiv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ) → ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
109 |
108
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) |
110 |
|
df-isom |
⊢ ( ( 𝐻 ∪ 𝐺 ) Isom 𝑅 , 𝑆 ( ( 𝐴 ∪ 𝐶 ) , ( 𝐵 ∪ 𝐷 ) ) ↔ ( ( 𝐻 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐶 ) ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ∪ 𝐺 ) ‘ 𝑦 ) ) ) ) |
111 |
14 109 110
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐻 ∪ 𝐺 ) Isom 𝑅 , 𝑆 ( ( 𝐴 ∪ 𝐶 ) , ( 𝐵 ∪ 𝐷 ) ) ) |