Step |
Hyp |
Ref |
Expression |
1 |
|
zorn2lem.3 |
⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ) |
2 |
|
zorn2lem.4 |
⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 } |
3 |
|
zorn2lem.5 |
⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } |
4 |
1 2 3
|
zorn2lem2 |
⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) ) |
6 |
3
|
ssrab3 |
⊢ 𝐷 ⊆ 𝐴 |
7 |
1 2 3
|
zorn2lem1 |
⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 ) |
8 |
6 7
|
sselid |
⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) |
9 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) ) |
10 |
9
|
biimprcd |
⊢ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) ) |
11 |
|
poirr |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) |
12 |
10 11
|
nsyli |
⊢ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ( ( 𝑅 Po 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |
13 |
12
|
com12 |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |
14 |
8 13
|
sylan2 |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |
15 |
5 14
|
syld |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |