Step |
Hyp |
Ref |
Expression |
1 |
|
onintrab2 |
⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ) |
2 |
1
|
biimpi |
⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ) |
3 |
2
|
adantr |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ) |
4 |
|
eloni |
⊢ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On → Ord ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
5 |
|
ordelss |
⊢ ( ( Ord ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
6 |
4 5
|
sylan |
⊢ ( ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
7 |
1 6
|
sylanb |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
8 |
|
ssdomg |
⊢ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On → ( 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → 𝑦 ≼ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
9 |
3 7 8
|
sylc |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ≼ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
10 |
|
onelon |
⊢ ( ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ∈ On ) |
11 |
1 10
|
sylanb |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ∈ On ) |
12 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐴 |
13 |
|
nfcv |
⊢ Ⅎ 𝑥 ≺ |
14 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } |
15 |
14
|
nfint |
⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } |
16 |
12 13 15
|
nfbr |
⊢ Ⅎ 𝑥 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } |
17 |
|
breq2 |
⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
18 |
16 17
|
onminsb |
⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
19 |
|
sdomentr |
⊢ ( ( 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∧ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) → 𝐴 ≺ 𝑦 ) |
20 |
18 19
|
sylan |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) → 𝐴 ≺ 𝑦 ) |
21 |
|
breq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ 𝑦 ) ) |
22 |
21
|
elrab |
⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) ) |
23 |
|
ssrab2 |
⊢ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ⊆ On |
24 |
|
onnmin |
⊢ ( ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ⊆ On ∧ 𝑦 ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
25 |
23 24
|
mpan |
⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
26 |
22 25
|
sylbir |
⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
27 |
26
|
expcom |
⊢ ( 𝐴 ≺ 𝑦 → ( 𝑦 ∈ On → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
28 |
20 27
|
syl |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) → ( 𝑦 ∈ On → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
29 |
28
|
impancom |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ On ) → ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
30 |
29
|
con2d |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) ) |
31 |
30
|
impancom |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ( 𝑦 ∈ On → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) ) |
32 |
11 31
|
mpd |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) |
33 |
|
ensym |
⊢ ( 𝑦 ≈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) |
34 |
32 33
|
nsyl |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ¬ 𝑦 ≈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
35 |
|
brsdom |
⊢ ( 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( 𝑦 ≼ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∧ ¬ 𝑦 ≈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
36 |
9 34 35
|
sylanbrc |
⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
37 |
36
|
ralrimiva |
⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
38 |
|
iscard |
⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) |
39 |
2 37 38
|
sylanbrc |
⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
40 |
|
vprc |
⊢ ¬ V ∈ V |
41 |
|
inteq |
⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∩ ∅ ) |
42 |
|
int0 |
⊢ ∩ ∅ = V |
43 |
41 42
|
eqtrdi |
⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = V ) |
44 |
43
|
eleq1d |
⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V ↔ V ∈ V ) ) |
45 |
40 44
|
mtbiri |
⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V ) |
46 |
|
fvex |
⊢ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ∈ V |
47 |
|
eleq1 |
⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ∈ V ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V ) ) |
48 |
46 47
|
mpbii |
⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V ) |
49 |
45 48
|
nsyl |
⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ¬ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
50 |
49
|
necon2ai |
⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≠ ∅ ) |
51 |
|
rabn0 |
⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ) |
52 |
50 51
|
sylib |
⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ) |
53 |
39 52
|
impbii |
⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |