| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eleq2 |
⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 +no 𝑐 ) ∈ 𝑥 ↔ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) |
| 2 |
1
|
ralbidv |
⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) |
| 3 |
|
eleq2 |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑏 +no 𝐶 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 4 |
3
|
ralbidv |
⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 5 |
2 4
|
anbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) ↔ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) ) |
| 6 |
5
|
onnminsb |
⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } → ¬ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) ) |
| 7 |
6
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } → ¬ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) ) |
| 8 |
|
naddov2 |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } ) |
| 9 |
8
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } ) |
| 10 |
9
|
eleq2d |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 +no 𝐶 ) ↔ 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } ) ) |
| 11 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ On ) |
| 12 |
|
onss |
⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On ) |
| 13 |
12
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐵 ⊆ On ) |
| 14 |
13
|
sselda |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ On ) |
| 15 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑏 ∈ 𝐵 ) → 𝐶 ∈ On ) |
| 16 |
14 15
|
naddcld |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 +no 𝐶 ) ∈ On ) |
| 17 |
|
ontri1 |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 +no 𝐶 ) ∈ On ) → ( 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ↔ ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 18 |
11 16 17
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ↔ ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 19 |
18
|
rexbidva |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ↔ ∃ 𝑏 ∈ 𝐵 ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 20 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 ∈ 𝐶 ) → 𝐴 ∈ On ) |
| 21 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 ∈ 𝐶 ) → 𝐵 ∈ On ) |
| 22 |
|
onss |
⊢ ( 𝐶 ∈ On → 𝐶 ⊆ On ) |
| 23 |
22
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐶 ⊆ On ) |
| 24 |
23
|
sselda |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ On ) |
| 25 |
21 24
|
naddcld |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝐵 +no 𝑐 ) ∈ On ) |
| 26 |
|
ontri1 |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +no 𝑐 ) ∈ On ) → ( 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ↔ ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) |
| 27 |
20 25 26
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ↔ ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) |
| 28 |
27
|
rexbidva |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ↔ ∃ 𝑐 ∈ 𝐶 ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) |
| 29 |
19 28
|
orbi12d |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∨ ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ↔ ( ∃ 𝑏 ∈ 𝐵 ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ∨ ∃ 𝑐 ∈ 𝐶 ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) ) |
| 30 |
|
orcom |
⊢ ( ( ¬ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ∨ ¬ ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ↔ ( ¬ ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∨ ¬ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 31 |
|
rexnal |
⊢ ( ∃ 𝑏 ∈ 𝐵 ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ↔ ¬ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) |
| 32 |
|
rexnal |
⊢ ( ∃ 𝑐 ∈ 𝐶 ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ↔ ¬ ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) |
| 33 |
31 32
|
orbi12i |
⊢ ( ( ∃ 𝑏 ∈ 𝐵 ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ∨ ∃ 𝑐 ∈ 𝐶 ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ↔ ( ¬ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ∨ ¬ ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ) |
| 34 |
|
ianor |
⊢ ( ¬ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ↔ ( ¬ ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∨ ¬ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 35 |
30 33 34
|
3bitr4i |
⊢ ( ( ∃ 𝑏 ∈ 𝐵 ¬ ( 𝑏 +no 𝐶 ) ∈ 𝐴 ∨ ∃ 𝑐 ∈ 𝐶 ¬ ( 𝐵 +no 𝑐 ) ∈ 𝐴 ) ↔ ¬ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) |
| 36 |
29 35
|
bitrdi |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∨ ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ↔ ¬ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝐴 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝐴 ) ) ) |
| 37 |
7 10 36
|
3imtr4d |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 +no 𝐶 ) → ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∨ ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) ) |
| 38 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) |
| 39 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝑏 ∈ 𝐵 ) |
| 40 |
14
|
adantrr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝑏 ∈ On ) |
| 41 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝐵 ∈ On ) |
| 42 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝐶 ∈ On ) |
| 43 |
|
naddel1 |
⊢ ( ( 𝑏 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 44 |
40 41 42 43
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 45 |
39 44
|
mpbid |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → ( 𝑏 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) |
| 46 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝐴 ∈ On ) |
| 47 |
|
naddcl |
⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) ∈ On ) |
| 48 |
47
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) ∈ On ) |
| 49 |
48
|
adantr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → ( 𝐵 +no 𝐶 ) ∈ On ) |
| 50 |
|
ontr2 |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +no 𝐶 ) ∈ On ) → ( ( 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∧ ( 𝑏 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 51 |
46 49 50
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → ( ( 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∧ ( 𝑏 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 52 |
38 45 51
|
mp2and |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) |
| 53 |
52
|
rexlimdvaa |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 54 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) |
| 55 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝑐 ∈ 𝐶 ) |
| 56 |
24
|
adantrr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝑐 ∈ On ) |
| 57 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝐶 ∈ On ) |
| 58 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝐵 ∈ On ) |
| 59 |
|
naddel2 |
⊢ ( ( 𝑐 ∈ On ∧ 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑐 ∈ 𝐶 ↔ ( 𝐵 +no 𝑐 ) ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 60 |
56 57 58 59
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → ( 𝑐 ∈ 𝐶 ↔ ( 𝐵 +no 𝑐 ) ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 61 |
55 60
|
mpbid |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → ( 𝐵 +no 𝑐 ) ∈ ( 𝐵 +no 𝐶 ) ) |
| 62 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝐴 ∈ On ) |
| 63 |
48
|
adantr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → ( 𝐵 +no 𝐶 ) ∈ On ) |
| 64 |
|
ontr2 |
⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 +no 𝐶 ) ∈ On ) → ( ( 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ∧ ( 𝐵 +no 𝑐 ) ∈ ( 𝐵 +no 𝐶 ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 65 |
62 63 64
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → ( ( 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ∧ ( 𝐵 +no 𝑐 ) ∈ ( 𝐵 +no 𝐶 ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 66 |
54 61 65
|
mp2and |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑐 ∈ 𝐶 ∧ 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) |
| 67 |
66
|
rexlimdvaa |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 68 |
53 67
|
jaod |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∨ ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) → 𝐴 ∈ ( 𝐵 +no 𝐶 ) ) ) |
| 69 |
37 68
|
impbid |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 +no 𝐶 ) ↔ ( ∃ 𝑏 ∈ 𝐵 𝐴 ⊆ ( 𝑏 +no 𝐶 ) ∨ ∃ 𝑐 ∈ 𝐶 𝐴 ⊆ ( 𝐵 +no 𝑐 ) ) ) ) |