Step |
Hyp |
Ref |
Expression |
1 |
|
frrlem11.1 |
⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |
2 |
|
frrlem11.2 |
⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 ) |
3 |
|
frrlem11.3 |
⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) |
4 |
|
frrlem11.4 |
⊢ 𝐶 = ( ( 𝐹 ↾ 𝑆 ) ∪ { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) |
5 |
|
frrlem12.5 |
⊢ ( 𝜑 → 𝑅 Fr 𝐴 ) |
6 |
|
frrlem12.6 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 ) |
7 |
|
frrlem12.7 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 ) |
8 |
|
frrlem13.8 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ∈ V ) |
9 |
|
frrlem13.9 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ⊆ 𝐴 ) |
10 |
|
frrlem14.10 |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) |
11 |
1 2
|
frrlem7 |
⊢ dom 𝐹 ⊆ 𝐴 |
12 |
11
|
a1i |
⊢ ( 𝜑 → dom 𝐹 ⊆ 𝐴 ) |
13 |
|
eldifn |
⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 ) |
14 |
13
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ¬ 𝑧 ∈ dom 𝐹 ) |
15 |
1 2 3 4 5 6 7 8 9
|
frrlem13 |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ∈ 𝐵 ) |
16 |
|
elssuni |
⊢ ( 𝐶 ∈ 𝐵 → 𝐶 ⊆ ∪ 𝐵 ) |
17 |
15 16
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ⊆ ∪ 𝐵 ) |
18 |
1 2
|
frrlem5 |
⊢ 𝐹 = ∪ 𝐵 |
19 |
17 18
|
sseqtrrdi |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ⊆ 𝐹 ) |
20 |
|
dmss |
⊢ ( 𝐶 ⊆ 𝐹 → dom 𝐶 ⊆ dom 𝐹 ) |
21 |
19 20
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → dom 𝐶 ⊆ dom 𝐹 ) |
22 |
|
ssun2 |
⊢ { 𝑧 } ⊆ ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } ) |
23 |
|
vsnid |
⊢ 𝑧 ∈ { 𝑧 } |
24 |
22 23
|
sselii |
⊢ 𝑧 ∈ ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } ) |
25 |
4
|
dmeqi |
⊢ dom 𝐶 = dom ( ( 𝐹 ↾ 𝑆 ) ∪ { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) |
26 |
|
dmun |
⊢ dom ( ( 𝐹 ↾ 𝑆 ) ∪ { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) = ( dom ( 𝐹 ↾ 𝑆 ) ∪ dom { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) |
27 |
|
ovex |
⊢ ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V |
28 |
27
|
dmsnop |
⊢ dom { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } = { 𝑧 } |
29 |
28
|
uneq2i |
⊢ ( dom ( 𝐹 ↾ 𝑆 ) ∪ dom { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) = ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } ) |
30 |
25 26 29
|
3eqtri |
⊢ dom 𝐶 = ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } ) |
31 |
24 30
|
eleqtrri |
⊢ 𝑧 ∈ dom 𝐶 |
32 |
31
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑧 ∈ dom 𝐶 ) |
33 |
21 32
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑧 ∈ dom 𝐹 ) |
34 |
33
|
expr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ → 𝑧 ∈ dom 𝐹 ) ) |
35 |
14 34
|
mtod |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ¬ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) |
36 |
35
|
nrexdv |
⊢ ( 𝜑 → ¬ ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) |
37 |
|
df-ne |
⊢ ( ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ↔ ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ ) |
38 |
37 10
|
sylan2br |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) |
39 |
38
|
ex |
⊢ ( 𝜑 → ( ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) |
40 |
36 39
|
mt3d |
⊢ ( 𝜑 → ( 𝐴 ∖ dom 𝐹 ) = ∅ ) |
41 |
|
ssdif0 |
⊢ ( 𝐴 ⊆ dom 𝐹 ↔ ( 𝐴 ∖ dom 𝐹 ) = ∅ ) |
42 |
40 41
|
sylibr |
⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 ) |
43 |
12 42
|
eqssd |
⊢ ( 𝜑 → dom 𝐹 = 𝐴 ) |