Step |
Hyp |
Ref |
Expression |
1 |
|
hauspwdom.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
1stcelcls |
⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐴 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) ) |
3 |
2
|
3adant1 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐴 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) ) |
4 |
|
uniexg |
⊢ ( 𝐽 ∈ Haus → ∪ 𝐽 ∈ V ) |
5 |
4
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ∪ 𝐽 ∈ V ) |
6 |
1 5
|
eqeltrid |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ V ) |
7 |
|
simp3 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 ) |
8 |
6 7
|
ssexd |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V ) |
9 |
|
nnex |
⊢ ℕ ∈ V |
10 |
|
elmapg |
⊢ ( ( 𝐴 ∈ V ∧ ℕ ∈ V ) → ( 𝑓 ∈ ( 𝐴 ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝐴 ) ) |
11 |
8 9 10
|
sylancl |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑓 ∈ ( 𝐴 ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝐴 ) ) |
12 |
11
|
anbi1d |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑓 ∈ ( 𝐴 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ↔ ( 𝑓 : ℕ ⟶ 𝐴 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) ) |
13 |
12
|
exbidv |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 ∈ ( 𝐴 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐴 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) ) |
14 |
3 13
|
bitr4d |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐴 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) ) |
15 |
|
df-rex |
⊢ ( ∃ 𝑓 ∈ ( 𝐴 ↑m ℕ ) 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐴 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) |
16 |
14 15
|
bitr4di |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∃ 𝑓 ∈ ( 𝐴 ↑m ℕ ) 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) |
17 |
|
vex |
⊢ 𝑥 ∈ V |
18 |
17
|
elima |
⊢ ( 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝐴 ↑m ℕ ) ) ↔ ∃ 𝑓 ∈ ( 𝐴 ↑m ℕ ) 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) |
19 |
16 18
|
bitr4di |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝐴 ↑m ℕ ) ) ) ) |
20 |
19
|
eqrdv |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝐴 ↑m ℕ ) ) ) |
21 |
|
ovex |
⊢ ( 𝐴 ↑m ℕ ) ∈ V |
22 |
|
lmfun |
⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) ) |
23 |
22
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → Fun ( ⇝𝑡 ‘ 𝐽 ) ) |
24 |
|
imadomg |
⊢ ( ( 𝐴 ↑m ℕ ) ∈ V → ( Fun ( ⇝𝑡 ‘ 𝐽 ) → ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝐴 ↑m ℕ ) ) ≼ ( 𝐴 ↑m ℕ ) ) ) |
25 |
21 23 24
|
mpsyl |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝐴 ↑m ℕ ) ) ≼ ( 𝐴 ↑m ℕ ) ) |
26 |
20 25
|
eqbrtrd |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) ) |