Step |
Hyp |
Ref |
Expression |
1 |
|
sltval |
⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) ) ) |
2 |
|
fvex |
⊢ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ V |
3 |
|
fvex |
⊢ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ V |
4 |
2 3
|
brtp |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ↔ ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o ) ) ) |
5 |
|
1n0 |
⊢ 1o ≠ ∅ |
6 |
5
|
neii |
⊢ ¬ 1o = ∅ |
7 |
|
eqeq1 |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ↔ 1o = ∅ ) ) |
8 |
6 7
|
mtbiri |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o → ¬ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) |
9 |
|
fvprc |
⊢ ( ¬ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) |
10 |
8 9
|
nsyl2 |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
11 |
10
|
adantr |
⊢ ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
12 |
10
|
adantr |
⊢ ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
13 |
|
2on0 |
⊢ 2o ≠ ∅ |
14 |
13
|
neii |
⊢ ¬ 2o = ∅ |
15 |
|
eqeq1 |
⊢ ( ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o → ( ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ↔ 2o = ∅ ) ) |
16 |
14 15
|
mtbiri |
⊢ ( ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o → ¬ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) |
17 |
|
fvprc |
⊢ ( ¬ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) |
18 |
16 17
|
nsyl2 |
⊢ ( ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
19 |
18
|
adantl |
⊢ ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
20 |
11 12 19
|
3jaoi |
⊢ ( ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2o ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
21 |
4 20
|
sylbi |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ) |
22 |
|
onintrab |
⊢ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ V ↔ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) |
23 |
21 22
|
sylib |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) |
24 |
23
|
adantl |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) |
25 |
|
onelon |
⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → 𝑦 ∈ On ) |
26 |
25
|
expcom |
⊢ ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On → 𝑦 ∈ On ) ) |
27 |
24 26
|
syl5 |
⊢ ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → 𝑦 ∈ On ) ) |
28 |
|
fveq2 |
⊢ ( 𝑎 = 𝑦 → ( 𝐴 ‘ 𝑎 ) = ( 𝐴 ‘ 𝑦 ) ) |
29 |
|
fveq2 |
⊢ ( 𝑎 = 𝑦 → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑦 ) ) |
30 |
28 29
|
neeq12d |
⊢ ( 𝑎 = 𝑦 → ( ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐴 ‘ 𝑦 ) ≠ ( 𝐵 ‘ 𝑦 ) ) ) |
31 |
30
|
onnminsb |
⊢ ( 𝑦 ∈ On → ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ¬ ( 𝐴 ‘ 𝑦 ) ≠ ( 𝐵 ‘ 𝑦 ) ) ) |
32 |
31
|
com12 |
⊢ ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝑦 ∈ On → ¬ ( 𝐴 ‘ 𝑦 ) ≠ ( 𝐵 ‘ 𝑦 ) ) ) |
33 |
27 32
|
syldc |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ¬ ( 𝐴 ‘ 𝑦 ) ≠ ( 𝐵 ‘ 𝑦 ) ) ) |
34 |
|
df-ne |
⊢ ( ( 𝐴 ‘ 𝑦 ) ≠ ( 𝐵 ‘ 𝑦 ) ↔ ¬ ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) |
35 |
34
|
con2bii |
⊢ ( ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ¬ ( 𝐴 ‘ 𝑦 ) ≠ ( 𝐵 ‘ 𝑦 ) ) |
36 |
33 35
|
syl6ibr |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) |
37 |
36
|
ralrimiv |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) |
38 |
24 37
|
jca |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) |
39 |
38
|
ex |
⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) ) |
40 |
39
|
impac |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ( ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
41 |
|
anass |
⊢ ( ( ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ↔ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) ) |
42 |
40 41
|
sylib |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) ) |
43 |
|
raleq |
⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ) |
44 |
|
fveq2 |
⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
45 |
|
fveq2 |
⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
46 |
44 45
|
breq12d |
⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
47 |
43 46
|
anbi12d |
⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) ) |
48 |
47
|
rspcev |
⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) ) |
49 |
42 48
|
syl |
⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) ) |
50 |
49
|
ex |
⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) ) ) |
51 |
|
eqeq12 |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = ∅ ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ 1o = ∅ ) ) |
52 |
6 51
|
mtbiri |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = ∅ ) → ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) |
53 |
|
1on |
⊢ 1o ∈ On |
54 |
|
0elon |
⊢ ∅ ∈ On |
55 |
|
suc11 |
⊢ ( ( 1o ∈ On ∧ ∅ ∈ On ) → ( suc 1o = suc ∅ ↔ 1o = ∅ ) ) |
56 |
55
|
necon3bid |
⊢ ( ( 1o ∈ On ∧ ∅ ∈ On ) → ( suc 1o ≠ suc ∅ ↔ 1o ≠ ∅ ) ) |
57 |
53 54 56
|
mp2an |
⊢ ( suc 1o ≠ suc ∅ ↔ 1o ≠ ∅ ) |
58 |
5 57
|
mpbir |
⊢ suc 1o ≠ suc ∅ |
59 |
|
df-2o |
⊢ 2o = suc 1o |
60 |
|
df-1o |
⊢ 1o = suc ∅ |
61 |
59 60
|
eqeq12i |
⊢ ( 2o = 1o ↔ suc 1o = suc ∅ ) |
62 |
58 61
|
nemtbir |
⊢ ¬ 2o = 1o |
63 |
|
eqeq12 |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ 1o = 2o ) ) |
64 |
|
eqcom |
⊢ ( 1o = 2o ↔ 2o = 1o ) |
65 |
63 64
|
bitrdi |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ 2o = 1o ) ) |
66 |
62 65
|
mtbiri |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) → ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) |
67 |
13
|
nesymi |
⊢ ¬ ∅ = 2o |
68 |
|
eqeq12 |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = ∅ ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ∅ = 2o ) ) |
69 |
67 68
|
mtbiri |
⊢ ( ( ( 𝐴 ‘ 𝑥 ) = ∅ ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) → ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) |
70 |
52 66 69
|
3jaoi |
⊢ ( ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = ∅ ) ∨ ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) ∨ ( ( 𝐴 ‘ 𝑥 ) = ∅ ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) ) → ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) |
71 |
|
fvex |
⊢ ( 𝐴 ‘ 𝑥 ) ∈ V |
72 |
|
fvex |
⊢ ( 𝐵 ‘ 𝑥 ) ∈ V |
73 |
71 72
|
brtp |
⊢ ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ↔ ( ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = ∅ ) ∨ ( ( 𝐴 ‘ 𝑥 ) = 1o ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) ∨ ( ( 𝐴 ‘ 𝑥 ) = ∅ ∧ ( 𝐵 ‘ 𝑥 ) = 2o ) ) ) |
74 |
|
df-ne |
⊢ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ) |
75 |
70 73 74
|
3imtr4i |
⊢ ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) → ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) |
76 |
|
fveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝐴 ‘ 𝑎 ) = ( 𝐴 ‘ 𝑥 ) ) |
77 |
|
fveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑥 ) ) |
78 |
76 77
|
neeq12d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) ) |
79 |
78
|
elrab |
⊢ ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ↔ ( 𝑥 ∈ On ∧ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) ) |
80 |
79
|
biimpri |
⊢ ( ( 𝑥 ∈ On ∧ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) → 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
81 |
80
|
adantlr |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) → 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
82 |
|
ssrab2 |
⊢ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ On |
83 |
|
ne0i |
⊢ ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ≠ ∅ ) |
84 |
83
|
adantl |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ≠ ∅ ) |
85 |
|
onint |
⊢ ( ( { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ On ∧ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ≠ ∅ ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
86 |
82 84 85
|
sylancr |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
87 |
|
nfrab1 |
⊢ Ⅎ 𝑎 { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } |
88 |
87
|
nfint |
⊢ Ⅎ 𝑎 ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } |
89 |
|
nfcv |
⊢ Ⅎ 𝑎 On |
90 |
|
nfcv |
⊢ Ⅎ 𝑎 𝐴 |
91 |
90 88
|
nffv |
⊢ Ⅎ 𝑎 ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
92 |
|
nfcv |
⊢ Ⅎ 𝑎 𝐵 |
93 |
92 88
|
nffv |
⊢ Ⅎ 𝑎 ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
94 |
91 93
|
nfne |
⊢ Ⅎ 𝑎 ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
95 |
|
fveq2 |
⊢ ( 𝑎 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑎 ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
96 |
|
fveq2 |
⊢ ( 𝑎 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
97 |
95 96
|
neeq12d |
⊢ ( 𝑎 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
98 |
88 89 94 97
|
elrabf |
⊢ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ↔ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
99 |
98
|
simprbi |
⊢ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
100 |
86 99
|
syl |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
101 |
|
df-ne |
⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ↔ ¬ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
102 |
100 101
|
sylib |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ¬ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
103 |
|
fveq2 |
⊢ ( 𝑦 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
104 |
|
fveq2 |
⊢ ( 𝑦 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐵 ‘ 𝑦 ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
105 |
103 104
|
eqeq12d |
⊢ ( 𝑦 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
106 |
105
|
rspccv |
⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ 𝑥 → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
107 |
106
|
ad2antlr |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ 𝑥 → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
108 |
102 107
|
mtod |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ¬ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ 𝑥 ) |
109 |
|
simpll |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → 𝑥 ∈ On ) |
110 |
|
oninton |
⊢ ( ( { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ On ∧ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ≠ ∅ ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) |
111 |
82 83 110
|
sylancr |
⊢ ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) |
112 |
111
|
adantl |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) |
113 |
|
ontri1 |
⊢ ( ( 𝑥 ∈ On ∧ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) → ( 𝑥 ⊆ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ↔ ¬ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ 𝑥 ) ) |
114 |
109 112 113
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝑥 ⊆ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ↔ ¬ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ 𝑥 ) ) |
115 |
108 114
|
mpbird |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → 𝑥 ⊆ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
116 |
|
intss1 |
⊢ ( 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ 𝑥 ) |
117 |
116
|
adantl |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ 𝑥 ) |
118 |
115 117
|
eqssd |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
119 |
81 118
|
syldan |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ) → 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
120 |
75 119
|
sylan2 |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) |
121 |
120
|
fveq2d |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
122 |
120
|
fveq2d |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
123 |
121 122
|
breq12d |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
124 |
123
|
biimpd |
⊢ ( ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
125 |
124
|
ex |
⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) → ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) → ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) ) |
126 |
125
|
pm2.43d |
⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) → ( ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
127 |
126
|
expimpd |
⊢ ( 𝑥 ∈ On → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |
128 |
127
|
rexlimiv |
⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) |
129 |
50 128
|
impbid1 |
⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ 𝑥 ) ) ) ) |
130 |
1 129
|
bitr4d |
⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) |