| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . 4
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝐴 ∈ FinIV) |
| 2 | | pssss 4098 |
. . . . . . . . 9
⊢ (𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵) |
| 3 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴) |
| 4 | 2, 3 | sylan9ssr 3998 |
. . . . . . . 8
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) → 𝑥 ⊆ 𝐴) |
| 5 | | difssd 4137 |
. . . . . . . 8
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) → (𝐴 ∖ 𝐵) ⊆ 𝐴) |
| 6 | 4, 5 | unssd 4192 |
. . . . . . 7
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) → (𝑥 ∪ (𝐴 ∖ 𝐵)) ⊆ 𝐴) |
| 7 | | pssnel 4471 |
. . . . . . . . 9
⊢ (𝑥 ⊊ 𝐵 → ∃𝑐(𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) |
| 8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) → ∃𝑐(𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) |
| 9 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → 𝐵 ⊆ 𝐴) |
| 10 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → 𝑐 ∈ 𝐵) |
| 11 | 9, 10 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → 𝑐 ∈ 𝐴) |
| 12 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → ¬ 𝑐 ∈ 𝑥) |
| 13 | | elndif 4133 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝐵 → ¬ 𝑐 ∈ (𝐴 ∖ 𝐵)) |
| 14 | 13 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → ¬ 𝑐 ∈ (𝐴 ∖ 𝐵)) |
| 15 | | ioran 986 |
. . . . . . . . . . . 12
⊢ (¬
(𝑐 ∈ 𝑥 ∨ 𝑐 ∈ (𝐴 ∖ 𝐵)) ↔ (¬ 𝑐 ∈ 𝑥 ∧ ¬ 𝑐 ∈ (𝐴 ∖ 𝐵))) |
| 16 | | elun 4153 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ (𝑥 ∪ (𝐴 ∖ 𝐵)) ↔ (𝑐 ∈ 𝑥 ∨ 𝑐 ∈ (𝐴 ∖ 𝐵))) |
| 17 | 15, 16 | xchnxbir 333 |
. . . . . . . . . . 11
⊢ (¬
𝑐 ∈ (𝑥 ∪ (𝐴 ∖ 𝐵)) ↔ (¬ 𝑐 ∈ 𝑥 ∧ ¬ 𝑐 ∈ (𝐴 ∖ 𝐵))) |
| 18 | 12, 14, 17 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → ¬ 𝑐 ∈ (𝑥 ∪ (𝐴 ∖ 𝐵))) |
| 19 | | nelneq2 2866 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ (𝑥 ∪ (𝐴 ∖ 𝐵))) → ¬ 𝐴 = (𝑥 ∪ (𝐴 ∖ 𝐵))) |
| 20 | 11, 18, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → ¬ 𝐴 = (𝑥 ∪ (𝐴 ∖ 𝐵))) |
| 21 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝐴 = (𝑥 ∪ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
| 22 | 20, 21 | sylnib 328 |
. . . . . . . 8
⊢ ((((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) ∧ (𝑐 ∈ 𝐵 ∧ ¬ 𝑐 ∈ 𝑥)) → ¬ (𝑥 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
| 23 | 8, 22 | exlimddv 1935 |
. . . . . . 7
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) → ¬ (𝑥 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
| 24 | | dfpss2 4088 |
. . . . . . 7
⊢ ((𝑥 ∪ (𝐴 ∖ 𝐵)) ⊊ 𝐴 ↔ ((𝑥 ∪ (𝐴 ∖ 𝐵)) ⊆ 𝐴 ∧ ¬ (𝑥 ∪ (𝐴 ∖ 𝐵)) = 𝐴)) |
| 25 | 6, 23, 24 | sylanbrc 583 |
. . . . . 6
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ 𝑥 ⊊ 𝐵) → (𝑥 ∪ (𝐴 ∖ 𝐵)) ⊊ 𝐴) |
| 26 | 25 | adantrr 717 |
. . . . 5
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑥 ∪ (𝐴 ∖ 𝐵)) ⊊ 𝐴) |
| 27 | | simprr 773 |
. . . . . . 7
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝑥 ≈ 𝐵) |
| 28 | | difexg 5329 |
. . . . . . . 8
⊢ (𝐴 ∈ FinIV →
(𝐴 ∖ 𝐵) ∈ V) |
| 29 | | enrefg 9024 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝐵) ∈ V → (𝐴 ∖ 𝐵) ≈ (𝐴 ∖ 𝐵)) |
| 30 | 1, 28, 29 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝐴 ∖ 𝐵) ≈ (𝐴 ∖ 𝐵)) |
| 31 | 2 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝑥 ⊆ 𝐵) |
| 32 | | ssinss1 4246 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐵 → (𝑥 ∩ 𝐴) ⊆ 𝐵) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑥 ∩ 𝐴) ⊆ 𝐵) |
| 34 | | inssdif0 4374 |
. . . . . . . . 9
⊢ ((𝑥 ∩ 𝐴) ⊆ 𝐵 ↔ (𝑥 ∩ (𝐴 ∖ 𝐵)) = ∅) |
| 35 | 33, 34 | sylib 218 |
. . . . . . . 8
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑥 ∩ (𝐴 ∖ 𝐵)) = ∅) |
| 36 | | disjdif 4472 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
| 37 | 35, 36 | jctir 520 |
. . . . . . 7
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → ((𝑥 ∩ (𝐴 ∖ 𝐵)) = ∅ ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅)) |
| 38 | | unen 9086 |
. . . . . . 7
⊢ (((𝑥 ≈ 𝐵 ∧ (𝐴 ∖ 𝐵) ≈ (𝐴 ∖ 𝐵)) ∧ ((𝑥 ∩ (𝐴 ∖ 𝐵)) = ∅ ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅)) → (𝑥 ∪ (𝐴 ∖ 𝐵)) ≈ (𝐵 ∪ (𝐴 ∖ 𝐵))) |
| 39 | 27, 30, 37, 38 | syl21anc 838 |
. . . . . 6
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑥 ∪ (𝐴 ∖ 𝐵)) ≈ (𝐵 ∪ (𝐴 ∖ 𝐵))) |
| 40 | | simplr 769 |
. . . . . . 7
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝐵 ⊆ 𝐴) |
| 41 | | undif 4482 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
| 42 | 40, 41 | sylib 218 |
. . . . . 6
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
| 43 | 39, 42 | breqtrd 5169 |
. . . . 5
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑥 ∪ (𝐴 ∖ 𝐵)) ≈ 𝐴) |
| 44 | | fin4i 10338 |
. . . . 5
⊢ (((𝑥 ∪ (𝐴 ∖ 𝐵)) ⊊ 𝐴 ∧ (𝑥 ∪ (𝐴 ∖ 𝐵)) ≈ 𝐴) → ¬ 𝐴 ∈ FinIV) |
| 45 | 26, 43, 44 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → ¬ 𝐴 ∈ FinIV) |
| 46 | 1, 45 | pm2.65da 817 |
. . 3
⊢ ((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) → ¬ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) |
| 47 | 46 | nexdv 1936 |
. 2
⊢ ((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) → ¬ ∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) |
| 48 | | ssexg 5323 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ FinIV) → 𝐵 ∈ V) |
| 49 | 48 | ancoms 458 |
. . 3
⊢ ((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
| 50 | | isfin4 10337 |
. . 3
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIV ↔
¬ ∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 51 | 49, 50 | syl 17 |
. 2
⊢ ((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) → (𝐵 ∈ FinIV ↔ ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 52 | 47, 51 | mpbird 257 |
1
⊢ ((𝐴 ∈ FinIV ∧
𝐵 ⊆ 𝐴) → 𝐵 ∈ FinIV) |