Step |
Hyp |
Ref |
Expression |
1 |
|
ssdif0 |
⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) = ∅ ) |
2 |
1
|
necon3bbii |
⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) |
3 |
|
difss |
⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 |
4 |
|
frmin |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) ) → ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) |
5 |
|
eldif |
⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) |
6 |
5
|
anbi1i |
⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ) |
7 |
|
anass |
⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝑦 ∈ 𝐵 ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ) ) |
8 |
|
ancom |
⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ↔ ( Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ∧ ¬ 𝑦 ∈ 𝐵 ) ) |
9 |
|
indif2 |
⊢ ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ( ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ 𝐴 ) ∖ 𝐵 ) |
10 |
|
df-pred |
⊢ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ( ( 𝐴 ∖ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) |
11 |
|
incom |
⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ ( 𝐴 ∖ 𝐵 ) ) |
12 |
10 11
|
eqtri |
⊢ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ ( 𝐴 ∖ 𝐵 ) ) |
13 |
|
df-pred |
⊢ Pred ( 𝑅 , 𝐴 , 𝑦 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) |
14 |
|
incom |
⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑦 } ) ) = ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ 𝐴 ) |
15 |
13 14
|
eqtri |
⊢ Pred ( 𝑅 , 𝐴 , 𝑦 ) = ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ 𝐴 ) |
16 |
15
|
difeq1i |
⊢ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) = ( ( ( ◡ 𝑅 “ { 𝑦 } ) ∩ 𝐴 ) ∖ 𝐵 ) |
17 |
9 12 16
|
3eqtr4i |
⊢ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) |
18 |
17
|
eqeq1i |
⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) = ∅ ) |
19 |
|
ssdif0 |
⊢ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) = ∅ ) |
20 |
18 19
|
bitr4i |
⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ) |
21 |
20
|
anbi1i |
⊢ ( ( Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ∧ ¬ 𝑦 ∈ 𝐵 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦 ∈ 𝐵 ) ) |
22 |
8 21
|
bitri |
⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦 ∈ 𝐵 ) ) |
23 |
22
|
anbi2i |
⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ¬ 𝑦 ∈ 𝐵 ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦 ∈ 𝐵 ) ) ) |
24 |
6 7 23
|
3bitri |
⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦 ∈ 𝐵 ) ) ) |
25 |
24
|
rexbii2 |
⊢ ( ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦 ∈ 𝐵 ) ) |
26 |
|
rexanali |
⊢ ( ∃ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦 ∈ 𝐵 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) |
27 |
25 26
|
bitri |
⊢ ( ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) Pred ( 𝑅 , ( 𝐴 ∖ 𝐵 ) , 𝑦 ) = ∅ ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) |
28 |
4 27
|
sylib |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) ) → ¬ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) |
29 |
28
|
ex |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → ¬ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) |
30 |
3 29
|
mpani |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( 𝐴 ∖ 𝐵 ) ≠ ∅ → ¬ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) |
31 |
2 30
|
syl5bi |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ¬ 𝐴 ⊆ 𝐵 → ¬ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) |
32 |
31
|
con4d |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) ) |
33 |
32
|
imp |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) → 𝐴 ⊆ 𝐵 ) |
34 |
33
|
adantrl |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) → 𝐴 ⊆ 𝐵 ) |
35 |
|
simprl |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) → 𝐵 ⊆ 𝐴 ) |
36 |
34 35
|
eqssd |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) → 𝐴 = 𝐵 ) |