Description: The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets).
This first section is dedicated to the construction of U and its intersection. First, the value of U at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | fin23lem.a | |- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t ) |
|
| Assertion | fin23lem12 | |- ( A e. _om -> ( U ` suc A ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fin23lem.a | |- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t ) |
|
| 2 | 1 | seqomsuc | |- ( A e. _om -> ( U ` suc A ) = ( A ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) ( U ` A ) ) ) |
| 3 | fvex | |- ( U ` A ) e. _V |
|
| 4 | fveq2 | |- ( i = A -> ( t ` i ) = ( t ` A ) ) |
|
| 5 | 4 | ineq1d | |- ( i = A -> ( ( t ` i ) i^i u ) = ( ( t ` A ) i^i u ) ) |
| 6 | 5 | eqeq1d | |- ( i = A -> ( ( ( t ` i ) i^i u ) = (/) <-> ( ( t ` A ) i^i u ) = (/) ) ) |
| 7 | 6 5 | ifbieq2d | |- ( i = A -> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) = if ( ( ( t ` A ) i^i u ) = (/) , u , ( ( t ` A ) i^i u ) ) ) |
| 8 | ineq2 | |- ( u = ( U ` A ) -> ( ( t ` A ) i^i u ) = ( ( t ` A ) i^i ( U ` A ) ) ) |
|
| 9 | 8 | eqeq1d | |- ( u = ( U ` A ) -> ( ( ( t ` A ) i^i u ) = (/) <-> ( ( t ` A ) i^i ( U ` A ) ) = (/) ) ) |
| 10 | id | |- ( u = ( U ` A ) -> u = ( U ` A ) ) |
|
| 11 | 9 10 8 | ifbieq12d | |- ( u = ( U ` A ) -> if ( ( ( t ` A ) i^i u ) = (/) , u , ( ( t ` A ) i^i u ) ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) ) |
| 12 | eqid | |- ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) = ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) |
|
| 13 | 3 | inex2 | |- ( ( t ` A ) i^i ( U ` A ) ) e. _V |
| 14 | 3 13 | ifex | |- if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) e. _V |
| 15 | 7 11 12 14 | ovmpo | |- ( ( A e. _om /\ ( U ` A ) e. _V ) -> ( A ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) ( U ` A ) ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) ) |
| 16 | 3 15 | mpan2 | |- ( A e. _om -> ( A ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) ( U ` A ) ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) ) |
| 17 | 2 16 | eqtrd | |- ( A e. _om -> ( U ` suc A ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) ) |