Step |
Hyp |
Ref |
Expression |
1 |
|
fnwe2.su |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 ) |
2 |
|
fnwe2.t |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) } |
3 |
|
fnwe2.s |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } ) |
4 |
|
fnwe2.f |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ) |
5 |
|
fnwe2.r |
⊢ ( 𝜑 → 𝑅 We 𝐵 ) |
6 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } ) |
7 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ) |
8 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → 𝑅 We 𝐵 ) |
9 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → 𝑎 ⊆ 𝐴 ) |
10 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → 𝑎 ≠ ∅ ) |
11 |
1 2 6 7 8 9 10
|
fnwe2lem2 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) |
12 |
11
|
ex |
⊢ ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) ) |
13 |
12
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) ) |
14 |
|
df-fr |
⊢ ( 𝑇 Fr 𝐴 ↔ ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) ) |
15 |
13 14
|
sylibr |
⊢ ( 𝜑 → 𝑇 Fr 𝐴 ) |
16 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } ) |
17 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ) |
18 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑅 We 𝐵 ) |
19 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑎 ∈ 𝐴 ) |
20 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 ∈ 𝐴 ) |
21 |
1 2 16 17 18 19 20
|
fnwe2lem3 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) ) |
22 |
21
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) ) |
23 |
|
dfwe2 |
⊢ ( 𝑇 We 𝐴 ↔ ( 𝑇 Fr 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) ) ) |
24 |
15 22 23
|
sylanbrc |
⊢ ( 𝜑 → 𝑇 We 𝐴 ) |