Step |
Hyp |
Ref |
Expression |
1 |
|
pmtrrn.t |
⊢ 𝑇 = ( pmTrsp ‘ 𝐷 ) |
2 |
|
pmtrrn.r |
⊢ 𝑅 = ran 𝑇 |
3 |
|
pmtrfrn.p |
⊢ 𝑃 = dom ( 𝐹 ∖ I ) |
4 |
|
noel |
⊢ ¬ 𝐹 ∈ ∅ |
5 |
1
|
rnfvprc |
⊢ ( ¬ 𝐷 ∈ V → ran 𝑇 = ∅ ) |
6 |
2 5
|
eqtrid |
⊢ ( ¬ 𝐷 ∈ V → 𝑅 = ∅ ) |
7 |
6
|
eleq2d |
⊢ ( ¬ 𝐷 ∈ V → ( 𝐹 ∈ 𝑅 ↔ 𝐹 ∈ ∅ ) ) |
8 |
4 7
|
mtbiri |
⊢ ( ¬ 𝐷 ∈ V → ¬ 𝐹 ∈ 𝑅 ) |
9 |
8
|
con4i |
⊢ ( 𝐹 ∈ 𝑅 → 𝐷 ∈ V ) |
10 |
|
mptexg |
⊢ ( 𝐷 ∈ V → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V ) |
11 |
10
|
ralrimivw |
⊢ ( 𝐷 ∈ V → ∀ 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V ) |
12 |
|
eqid |
⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) |
13 |
12
|
fnmpt |
⊢ ( ∀ 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V → ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ) |
14 |
11 13
|
syl |
⊢ ( 𝐷 ∈ V → ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ) |
15 |
1
|
pmtrfval |
⊢ ( 𝐷 ∈ V → 𝑇 = ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) ) |
16 |
15
|
fneq1d |
⊢ ( 𝐷 ∈ V → ( 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↔ ( 𝑤 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑤 , ∪ ( 𝑤 ∖ { 𝑧 } ) , 𝑧 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ) ) |
17 |
14 16
|
mpbird |
⊢ ( 𝐷 ∈ V → 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ) |
18 |
|
fvelrnb |
⊢ ( 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } → ( 𝐹 ∈ ran 𝑇 ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑇 ‘ 𝑦 ) = 𝐹 ) ) |
19 |
17 18
|
syl |
⊢ ( 𝐷 ∈ V → ( 𝐹 ∈ ran 𝑇 ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑇 ‘ 𝑦 ) = 𝐹 ) ) |
20 |
2
|
eleq2i |
⊢ ( 𝐹 ∈ 𝑅 ↔ 𝐹 ∈ ran 𝑇 ) |
21 |
|
breq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 2o ↔ 𝑦 ≈ 2o ) ) |
22 |
21
|
rexrab |
⊢ ( ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑇 ‘ 𝑦 ) = 𝐹 ↔ ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇 ‘ 𝑦 ) = 𝐹 ) ) |
23 |
22
|
bicomi |
⊢ ( ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇 ‘ 𝑦 ) = 𝐹 ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑇 ‘ 𝑦 ) = 𝐹 ) |
24 |
19 20 23
|
3bitr4g |
⊢ ( 𝐷 ∈ V → ( 𝐹 ∈ 𝑅 ↔ ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇 ‘ 𝑦 ) = 𝐹 ) ) ) |
25 |
|
elpwi |
⊢ ( 𝑦 ∈ 𝒫 𝐷 → 𝑦 ⊆ 𝐷 ) |
26 |
|
simp1 |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → 𝐷 ∈ V ) |
27 |
1
|
pmtrmvd |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑦 ) |
28 |
|
simp2 |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → 𝑦 ⊆ 𝐷 ) |
29 |
27 28
|
eqsstrd |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ) |
30 |
|
simp3 |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → 𝑦 ≈ 2o ) |
31 |
27 30
|
eqbrtrd |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) |
32 |
26 29 31
|
3jca |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → ( 𝐷 ∈ V ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) ) |
33 |
27
|
eqcomd |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → 𝑦 = dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) |
34 |
33
|
fveq2d |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) ) |
35 |
32 34
|
jca |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) ∧ ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) ) ) |
36 |
|
difeq1 |
⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝐹 → ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = ( 𝐹 ∖ I ) ) |
37 |
36
|
dmeqd |
⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝐹 → dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = dom ( 𝐹 ∖ I ) ) |
38 |
37 3
|
eqtr4di |
⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝐹 → dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 ) |
39 |
|
sseq1 |
⊢ ( dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 → ( dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ↔ 𝑃 ⊆ 𝐷 ) ) |
40 |
|
breq1 |
⊢ ( dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 → ( dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ↔ 𝑃 ≈ 2o ) ) |
41 |
39 40
|
3anbi23d |
⊢ ( dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 → ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) ↔ ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ) ) |
42 |
41
|
adantl |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) = 𝐹 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 ) → ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) ↔ ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ) ) |
43 |
|
simpl |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) = 𝐹 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 ) → ( 𝑇 ‘ 𝑦 ) = 𝐹 ) |
44 |
|
fveq2 |
⊢ ( dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 → ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) = ( 𝑇 ‘ 𝑃 ) ) |
45 |
44
|
adantl |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) = 𝐹 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 ) → ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) = ( 𝑇 ‘ 𝑃 ) ) |
46 |
43 45
|
eqeq12d |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) = 𝐹 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 ) → ( ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) ↔ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) |
47 |
42 46
|
anbi12d |
⊢ ( ( ( 𝑇 ‘ 𝑦 ) = 𝐹 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) = 𝑃 ) → ( ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) ∧ ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) ) ↔ ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) |
48 |
38 47
|
mpdan |
⊢ ( ( 𝑇 ‘ 𝑦 ) = 𝐹 → ( ( ( 𝐷 ∈ V ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ⊆ 𝐷 ∧ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ≈ 2o ) ∧ ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ dom ( ( 𝑇 ‘ 𝑦 ) ∖ I ) ) ) ↔ ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) |
49 |
35 48
|
syl5ibcom |
⊢ ( ( 𝐷 ∈ V ∧ 𝑦 ⊆ 𝐷 ∧ 𝑦 ≈ 2o ) → ( ( 𝑇 ‘ 𝑦 ) = 𝐹 → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) |
50 |
49
|
3exp |
⊢ ( 𝐷 ∈ V → ( 𝑦 ⊆ 𝐷 → ( 𝑦 ≈ 2o → ( ( 𝑇 ‘ 𝑦 ) = 𝐹 → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) ) ) |
51 |
50
|
imp4a |
⊢ ( 𝐷 ∈ V → ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ≈ 2o ∧ ( 𝑇 ‘ 𝑦 ) = 𝐹 ) → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) ) |
52 |
25 51
|
syl5 |
⊢ ( 𝐷 ∈ V → ( 𝑦 ∈ 𝒫 𝐷 → ( ( 𝑦 ≈ 2o ∧ ( 𝑇 ‘ 𝑦 ) = 𝐹 ) → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) ) |
53 |
52
|
rexlimdv |
⊢ ( 𝐷 ∈ V → ( ∃ 𝑦 ∈ 𝒫 𝐷 ( 𝑦 ≈ 2o ∧ ( 𝑇 ‘ 𝑦 ) = 𝐹 ) → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) |
54 |
24 53
|
sylbid |
⊢ ( 𝐷 ∈ V → ( 𝐹 ∈ 𝑅 → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) ) |
55 |
9 54
|
mpcom |
⊢ ( 𝐹 ∈ 𝑅 → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) ) |