| Step |
Hyp |
Ref |
Expression |
| 1 |
|
utoptop.1 |
⊢ 𝐽 = ( unifTop ‘ 𝑈 ) |
| 2 |
|
relxp |
⊢ Rel ( 𝑋 × 𝑋 ) |
| 3 |
|
utoptop |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top ) |
| 4 |
1 3
|
eqeltrid |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
| 5 |
|
txtop |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐽 ×t 𝐽 ) ∈ Top ) |
| 6 |
4 4 5
|
syl2anc |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐽 ×t 𝐽 ) ∈ Top ) |
| 7 |
6
|
ad3antrrr |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( 𝐽 ×t 𝐽 ) ∈ Top ) |
| 8 |
|
simpllr |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) |
| 9 |
|
utoptopon |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ ( TopOn ‘ 𝑋 ) ) |
| 10 |
1 9
|
eqeltrid |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
| 11 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
| 12 |
10 11
|
syl |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
| 13 |
12
|
sqxpeqd |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ( ∪ 𝐽 × ∪ 𝐽 ) ) |
| 14 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
| 15 |
14 14
|
txuni |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( ∪ 𝐽 × ∪ 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 ) ) |
| 16 |
4 4 15
|
syl2anc |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∪ 𝐽 × ∪ 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 ) ) |
| 17 |
13 16
|
eqtrd |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ∪ ( 𝐽 ×t 𝐽 ) ) |
| 18 |
17
|
ad3antrrr |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( 𝑋 × 𝑋 ) = ∪ ( 𝐽 ×t 𝐽 ) ) |
| 19 |
8 18
|
sseqtrd |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑀 ⊆ ∪ ( 𝐽 ×t 𝐽 ) ) |
| 20 |
|
eqid |
⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 ) |
| 21 |
20
|
clsss3 |
⊢ ( ( ( 𝐽 ×t 𝐽 ) ∈ Top ∧ 𝑀 ⊆ ∪ ( 𝐽 ×t 𝐽 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ∪ ( 𝐽 ×t 𝐽 ) ) |
| 22 |
7 19 21
|
syl2anc |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ∪ ( 𝐽 ×t 𝐽 ) ) |
| 23 |
22 18
|
sseqtrrd |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝑋 × 𝑋 ) ) |
| 24 |
|
simpr |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) |
| 25 |
23 24
|
sseldd |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 ∈ ( 𝑋 × 𝑋 ) ) |
| 26 |
|
1st2nd |
⊢ ( ( Rel ( 𝑋 × 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) |
| 27 |
2 25 26
|
sylancr |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) |
| 28 |
|
simplll |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
| 29 |
|
simplrl |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑉 ∈ 𝑈 ) |
| 30 |
4
|
3ad2ant1 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → 𝐽 ∈ Top ) |
| 31 |
|
xp1st |
⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( 1st ‘ 𝑧 ) ∈ 𝑋 ) |
| 32 |
1
|
utopsnnei |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ ( 1st ‘ 𝑧 ) ∈ 𝑋 ) → ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1st ‘ 𝑧 ) } ) ) |
| 33 |
31 32
|
syl3an3 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1st ‘ 𝑧 ) } ) ) |
| 34 |
|
xp2nd |
⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( 2nd ‘ 𝑧 ) ∈ 𝑋 ) |
| 35 |
1
|
utopsnnei |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑋 ) → ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2nd ‘ 𝑧 ) } ) ) |
| 36 |
34 35
|
syl3an3 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2nd ‘ 𝑧 ) } ) ) |
| 37 |
14 14
|
neitx |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) ∧ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1st ‘ 𝑧 ) } ) ∧ ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2nd ‘ 𝑧 ) } ) ) ) → ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st ‘ 𝑧 ) } × { ( 2nd ‘ 𝑧 ) } ) ) ) |
| 38 |
30 30 33 36 37
|
syl22anc |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st ‘ 𝑧 ) } × { ( 2nd ‘ 𝑧 ) } ) ) ) |
| 39 |
|
1st2nd2 |
⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) |
| 40 |
39
|
sneqd |
⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → { 𝑧 } = { ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ } ) |
| 41 |
|
fvex |
⊢ ( 1st ‘ 𝑧 ) ∈ V |
| 42 |
|
fvex |
⊢ ( 2nd ‘ 𝑧 ) ∈ V |
| 43 |
41 42
|
xpsn |
⊢ ( { ( 1st ‘ 𝑧 ) } × { ( 2nd ‘ 𝑧 ) } ) = { ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ } |
| 44 |
40 43
|
eqtr4di |
⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → { 𝑧 } = ( { ( 1st ‘ 𝑧 ) } × { ( 2nd ‘ 𝑧 ) } ) ) |
| 45 |
44
|
fveq2d |
⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) = ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st ‘ 𝑧 ) } × { ( 2nd ‘ 𝑧 ) } ) ) ) |
| 46 |
45
|
3ad2ant3 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) = ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( { ( 1st ‘ 𝑧 ) } × { ( 2nd ‘ 𝑧 ) } ) ) ) |
| 47 |
38 46
|
eleqtrrd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) ) |
| 48 |
28 29 25 47
|
syl3anc |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) ) |
| 49 |
20
|
neindisj |
⊢ ( ( ( ( 𝐽 ×t 𝐽 ) ∈ Top ∧ 𝑀 ⊆ ∪ ( 𝐽 ×t 𝐽 ) ) ∧ ( 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ∧ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐽 ) ) ‘ { 𝑧 } ) ) ) → ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ≠ ∅ ) |
| 50 |
7 19 24 48 49
|
syl22anc |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ≠ ∅ ) |
| 51 |
|
simp-4l |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
| 52 |
|
simpr1l |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) ) → 𝑉 ∈ 𝑈 ) |
| 53 |
52
|
3anassrs |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑉 ∈ 𝑈 ) |
| 54 |
|
ustrel |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → Rel 𝑉 ) |
| 55 |
51 53 54
|
syl2anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → Rel 𝑉 ) |
| 56 |
|
simpr |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) |
| 57 |
|
elin |
⊢ ( 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ↔ ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∧ 𝑟 ∈ 𝑀 ) ) |
| 58 |
56 57
|
sylib |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∧ 𝑟 ∈ 𝑀 ) ) |
| 59 |
58
|
simpld |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑟 ∈ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ) |
| 60 |
|
xp1st |
⊢ ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) → ( 1st ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ) |
| 61 |
59 60
|
syl |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ) |
| 62 |
|
elrelimasn |
⊢ ( Rel 𝑉 → ( ( 1st ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ↔ ( 1st ‘ 𝑧 ) 𝑉 ( 1st ‘ 𝑟 ) ) ) |
| 63 |
62
|
biimpa |
⊢ ( ( Rel 𝑉 ∧ ( 1st ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) ) → ( 1st ‘ 𝑧 ) 𝑉 ( 1st ‘ 𝑟 ) ) |
| 64 |
55 61 63
|
syl2anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st ‘ 𝑧 ) 𝑉 ( 1st ‘ 𝑟 ) ) |
| 65 |
|
simp-4r |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) |
| 66 |
|
xpss |
⊢ ( 𝑋 × 𝑋 ) ⊆ ( V × V ) |
| 67 |
65 66
|
sstrdi |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑀 ⊆ ( V × V ) ) |
| 68 |
|
df-rel |
⊢ ( Rel 𝑀 ↔ 𝑀 ⊆ ( V × V ) ) |
| 69 |
67 68
|
sylibr |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → Rel 𝑀 ) |
| 70 |
58
|
simprd |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → 𝑟 ∈ 𝑀 ) |
| 71 |
|
1st2ndbr |
⊢ ( ( Rel 𝑀 ∧ 𝑟 ∈ 𝑀 ) → ( 1st ‘ 𝑟 ) 𝑀 ( 2nd ‘ 𝑟 ) ) |
| 72 |
69 70 71
|
syl2anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st ‘ 𝑟 ) 𝑀 ( 2nd ‘ 𝑟 ) ) |
| 73 |
|
xp2nd |
⊢ ( 𝑟 ∈ ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) → ( 2nd ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) |
| 74 |
59 73
|
syl |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 2nd ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) |
| 75 |
|
elrelimasn |
⊢ ( Rel 𝑉 → ( ( 2nd ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ↔ ( 2nd ‘ 𝑧 ) 𝑉 ( 2nd ‘ 𝑟 ) ) ) |
| 76 |
75
|
biimpa |
⊢ ( ( Rel 𝑉 ∧ ( 2nd ‘ 𝑟 ) ∈ ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) → ( 2nd ‘ 𝑧 ) 𝑉 ( 2nd ‘ 𝑟 ) ) |
| 77 |
55 74 76
|
syl2anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 2nd ‘ 𝑧 ) 𝑉 ( 2nd ‘ 𝑟 ) ) |
| 78 |
|
simpr1r |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) ) → ◡ 𝑉 = 𝑉 ) |
| 79 |
78
|
3anassrs |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ◡ 𝑉 = 𝑉 ) |
| 80 |
|
breq |
⊢ ( ◡ 𝑉 = 𝑉 → ( ( 2nd ‘ 𝑟 ) ◡ 𝑉 ( 2nd ‘ 𝑧 ) ↔ ( 2nd ‘ 𝑟 ) 𝑉 ( 2nd ‘ 𝑧 ) ) ) |
| 81 |
|
fvex |
⊢ ( 2nd ‘ 𝑟 ) ∈ V |
| 82 |
81 42
|
brcnv |
⊢ ( ( 2nd ‘ 𝑟 ) ◡ 𝑉 ( 2nd ‘ 𝑧 ) ↔ ( 2nd ‘ 𝑧 ) 𝑉 ( 2nd ‘ 𝑟 ) ) |
| 83 |
80 82
|
bitr3di |
⊢ ( ◡ 𝑉 = 𝑉 → ( ( 2nd ‘ 𝑟 ) 𝑉 ( 2nd ‘ 𝑧 ) ↔ ( 2nd ‘ 𝑧 ) 𝑉 ( 2nd ‘ 𝑟 ) ) ) |
| 84 |
79 83
|
syl |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( ( 2nd ‘ 𝑟 ) 𝑉 ( 2nd ‘ 𝑧 ) ↔ ( 2nd ‘ 𝑧 ) 𝑉 ( 2nd ‘ 𝑟 ) ) ) |
| 85 |
77 84
|
mpbird |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 2nd ‘ 𝑟 ) 𝑉 ( 2nd ‘ 𝑧 ) ) |
| 86 |
|
fvex |
⊢ ( 1st ‘ 𝑟 ) ∈ V |
| 87 |
41 86 81
|
brcoi |
⊢ ( ( ( 1st ‘ 𝑧 ) 𝑉 ( 1st ‘ 𝑟 ) ∧ ( 1st ‘ 𝑟 ) 𝑀 ( 2nd ‘ 𝑟 ) ) → ( 1st ‘ 𝑧 ) ( 𝑀 ∘ 𝑉 ) ( 2nd ‘ 𝑟 ) ) |
| 88 |
41 81 42
|
brcoi |
⊢ ( ( ( 1st ‘ 𝑧 ) ( 𝑀 ∘ 𝑉 ) ( 2nd ‘ 𝑟 ) ∧ ( 2nd ‘ 𝑟 ) 𝑉 ( 2nd ‘ 𝑧 ) ) → ( 1st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2nd ‘ 𝑧 ) ) |
| 89 |
87 88
|
sylan |
⊢ ( ( ( ( 1st ‘ 𝑧 ) 𝑉 ( 1st ‘ 𝑟 ) ∧ ( 1st ‘ 𝑟 ) 𝑀 ( 2nd ‘ 𝑟 ) ) ∧ ( 2nd ‘ 𝑟 ) 𝑉 ( 2nd ‘ 𝑧 ) ) → ( 1st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2nd ‘ 𝑧 ) ) |
| 90 |
64 72 85 89
|
syl21anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) ∧ 𝑟 ∈ ( ( ( 𝑉 “ { ( 1st ‘ 𝑧 ) } ) × ( 𝑉 “ { ( 2nd ‘ 𝑧 ) } ) ) ∩ 𝑀 ) ) → ( 1st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2nd ‘ 𝑧 ) ) |
| 91 |
50 90
|
n0limd |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ( 1st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2nd ‘ 𝑧 ) ) |
| 92 |
|
df-br |
⊢ ( ( 1st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2nd ‘ 𝑧 ) ↔ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ) |
| 93 |
91 92
|
sylib |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ) |
| 94 |
27 93
|
eqeltrd |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) ∧ 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ) → 𝑧 ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ) |
| 95 |
94
|
ex |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) → ( 𝑧 ∈ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) → 𝑧 ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ) ) |
| 96 |
95
|
ssrdv |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ◡ 𝑉 = 𝑉 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ) |