Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
โข โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)} = โช โฉ {๐
โ On โฃ ๐ต โ
(๐ด โo ๐)} |
2 | 1 | oeeulem 8553 |
. . . 4
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (โช โฉ {๐
โ On โฃ ๐ต โ
(๐ด โo ๐)} โ On โง (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) โ ๐ต โง ๐ต โ (๐ด โo suc โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}))) |
3 | 2 | simp1d 1143 |
. . 3
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ โช โฉ {๐
โ On โฃ ๐ต โ
(๐ด โo ๐)} โ On) |
4 | | fvexd 6862 |
. . 3
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (1st โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) โ V) |
5 | | fvexd 6862 |
. . 3
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (2nd โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) โ V) |
6 | | eqid 2737 |
. . . 4
โข
(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต)) = (โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต)) |
7 | | eqid 2737 |
. . . 4
โข
(1st โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) = (1st โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) |
8 | | eqid 2737 |
. . . 4
โข
(2nd โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) = (2nd โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) |
9 | 1, 6, 7, 8 | oeeui 8554 |
. . 3
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต) โ (๐ฅ = โช โฉ {๐
โ On โฃ ๐ต โ
(๐ด โo ๐)} โง ๐ฆ = (1st โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต))) โง ๐ง = (2nd โ(โฉ๐โ๐ โ On โ๐ โ (๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)})(๐ = โจ๐, ๐โฉ โง (((๐ด โo โช โฉ {๐ โ On โฃ ๐ต โ (๐ด โo ๐)}) ยทo ๐) +o ๐) = ๐ต)))))) |
10 | 3, 4, 5, 9 | euotd 5475 |
. 2
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ โ!๐คโ๐ฅโ๐ฆโ๐ง(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
11 | | df-3an 1090 |
. . . . . . . . . . 11
โข ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โ ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง ๐ง โ (๐ด โo ๐ฅ))) |
12 | 11 | biancomi 464 |
. . . . . . . . . 10
โข ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โ (๐ง โ (๐ด โo ๐ฅ) โง (๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)))) |
13 | 12 | anbi1i 625 |
. . . . . . . . 9
โข (((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต) โ ((๐ง โ (๐ด โo ๐ฅ) โง (๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o))) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) |
14 | 13 | anbi2i 624 |
. . . . . . . 8
โข ((๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ง โ (๐ด โo ๐ฅ) โง (๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o))) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
15 | | an12 644 |
. . . . . . . 8
โข ((๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ง โ (๐ด โo ๐ฅ) โง (๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o))) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ ((๐ง โ (๐ด โo ๐ฅ) โง (๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o))) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
16 | | anass 470 |
. . . . . . . 8
โข (((๐ง โ (๐ด โo ๐ฅ) โง (๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o))) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ (๐ง โ (๐ด โo ๐ฅ) โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)))) |
17 | 14, 15, 16 | 3bitri 297 |
. . . . . . 7
โข ((๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ (๐ง โ (๐ด โo ๐ฅ) โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)))) |
18 | 17 | exbii 1851 |
. . . . . 6
โข
(โ๐ง(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ โ๐ง(๐ง โ (๐ด โo ๐ฅ) โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)))) |
19 | | df-rex 3075 |
. . . . . 6
โข
(โ๐ง โ
(๐ด โo ๐ฅ)((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ โ๐ง(๐ง โ (๐ด โo ๐ฅ) โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)))) |
20 | | r19.42v 3188 |
. . . . . 6
โข
(โ๐ง โ
(๐ด โo ๐ฅ)((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง (๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
21 | 18, 19, 20 | 3bitr2i 299 |
. . . . 5
โข
(โ๐ง(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
22 | 21 | 2exbii 1852 |
. . . 4
โข
(โ๐ฅโ๐ฆโ๐ง(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ โ๐ฅโ๐ฆ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
23 | | r2ex 3193 |
. . . 4
โข
(โ๐ฅ โ On
โ๐ฆ โ (๐ด โ
1o)โ๐ง
โ (๐ด
โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต) โ โ๐ฅโ๐ฆ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o)) โง โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต))) |
24 | 22, 23 | bitr4i 278 |
. . 3
โข
(โ๐ฅโ๐ฆโ๐ง(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ โ๐ฅ โ On โ๐ฆ โ (๐ด โ 1o)โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) |
25 | 24 | eubii 2584 |
. 2
โข
(โ!๐คโ๐ฅโ๐ฆโ๐ง(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง ((๐ฅ โ On โง ๐ฆ โ (๐ด โ 1o) โง ๐ง โ (๐ด โo ๐ฅ)) โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) โ โ!๐คโ๐ฅ โ On โ๐ฆ โ (๐ด โ 1o)โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) |
26 | 10, 25 | sylib 217 |
1
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ โ!๐คโ๐ฅ โ On โ๐ฆ โ (๐ด โ 1o)โ๐ง โ (๐ด โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((๐ด โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ต)) |