Step |
Hyp |
Ref |
Expression |
1 |
|
df-fin5 |
⊢ FinV = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) } |
2 |
1
|
eleq2i |
⊢ ( 𝐴 ∈ FinV ↔ 𝐴 ∈ { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) } ) |
3 |
|
id |
⊢ ( 𝐴 = ∅ → 𝐴 = ∅ ) |
4 |
|
0ex |
⊢ ∅ ∈ V |
5 |
3 4
|
eqeltrdi |
⊢ ( 𝐴 = ∅ → 𝐴 ∈ V ) |
6 |
|
relsdom |
⊢ Rel ≺ |
7 |
6
|
brrelex1i |
⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → 𝐴 ∈ V ) |
8 |
5 7
|
jaoi |
⊢ ( ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) → 𝐴 ∈ V ) |
9 |
|
eqeq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ∅ ↔ 𝐴 = ∅ ) ) |
10 |
|
id |
⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 ) |
11 |
|
djueq12 |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑥 ⊔ 𝑥 ) = ( 𝐴 ⊔ 𝐴 ) ) |
12 |
11
|
anidms |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊔ 𝑥 ) = ( 𝐴 ⊔ 𝐴 ) ) |
13 |
10 12
|
breq12d |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ↔ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) ) |
14 |
9 13
|
orbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) ) ) |
15 |
8 14
|
elab3 |
⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) } ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) ) |
16 |
2 15
|
bitri |
⊢ ( 𝐴 ∈ FinV ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) ) |