Step |
Hyp |
Ref |
Expression |
1 |
|
nosepon |
⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On ) |
2 |
|
onelon |
⊢ ( ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On ∧ 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → 𝑋 ∈ On ) |
3 |
1 2
|
sylan |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → 𝑋 ∈ On ) |
4 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) |
5 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) ) |
6 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑋 ) ) |
7 |
5 6
|
neeq12d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐵 ‘ 𝑋 ) ) ) |
8 |
7
|
onnminsb |
⊢ ( 𝑋 ∈ On → ( 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } → ¬ ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐵 ‘ 𝑋 ) ) ) |
9 |
3 4 8
|
sylc |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ¬ ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐵 ‘ 𝑋 ) ) |
10 |
|
df-ne |
⊢ ( ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐵 ‘ 𝑋 ) ↔ ¬ ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) |
11 |
10
|
con2bii |
⊢ ( ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ↔ ¬ ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐵 ‘ 𝑋 ) ) |
12 |
9 11
|
sylibr |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( 𝐴 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) |