Step |
Hyp |
Ref |
Expression |
1 |
|
ptcmp.1 |
⊢ 𝑆 = ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) |
2 |
|
ptcmp.2 |
⊢ 𝑋 = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) |
3 |
|
ptcmp.3 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
4 |
|
ptcmp.4 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Comp ) |
5 |
|
ptcmp.5 |
⊢ ( 𝜑 → 𝑋 ∈ ( UFL ∩ dom card ) ) |
6 |
|
ptcmplem2.5 |
⊢ ( 𝜑 → 𝑈 ⊆ ran 𝑆 ) |
7 |
|
ptcmplem2.6 |
⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 ) |
8 |
|
ptcmplem2.7 |
⊢ ( 𝜑 → ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 ) |
9 |
|
0ss |
⊢ ∅ ⊆ 𝑈 |
10 |
|
0fin |
⊢ ∅ ∈ Fin |
11 |
|
elfpw |
⊢ ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( ∅ ⊆ 𝑈 ∧ ∅ ∈ Fin ) ) |
12 |
9 10 11
|
mpbir2an |
⊢ ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) |
13 |
|
unieq |
⊢ ( 𝑧 = ∅ → ∪ 𝑧 = ∪ ∅ ) |
14 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
15 |
13 14
|
eqtrdi |
⊢ ( 𝑧 = ∅ → ∪ 𝑧 = ∅ ) |
16 |
15
|
rspceeqv |
⊢ ( ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑋 = ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 ) |
17 |
12 16
|
mpan |
⊢ ( 𝑋 = ∅ → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 ) |
18 |
17
|
necon3bi |
⊢ ( ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 → 𝑋 ≠ ∅ ) |
19 |
8 18
|
syl |
⊢ ( 𝜑 → 𝑋 ≠ ∅ ) |
20 |
|
n0 |
⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ 𝑋 ) |
21 |
19 20
|
sylib |
⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ 𝑋 ) |
22 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) |
23 |
22
|
unieqd |
⊢ ( 𝑛 = 𝑘 → ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
24 |
23
|
cbvixpv |
⊢ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) |
25 |
2 24
|
eqtri |
⊢ 𝑋 = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) |
26 |
5
|
elin2d |
⊢ ( 𝜑 → 𝑋 ∈ dom card ) |
27 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ∈ dom card ) |
28 |
25 27
|
eqeltrrid |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ) |
29 |
|
ssrab2 |
⊢ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ 𝐴 |
30 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ≠ ∅ ) |
31 |
25 30
|
eqnetrrid |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ ) |
32 |
|
eqid |
⊢ ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) = ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) |
33 |
32
|
resixpfo |
⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ 𝐴 ∧ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ ) → ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) : X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) –onto→ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ) |
34 |
29 31 33
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) : X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) –onto→ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ) |
35 |
|
fonum |
⊢ ( ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ∧ ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) : X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) –onto→ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ) → X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ) |
36 |
28 34 35
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ) |
37 |
|
vex |
⊢ 𝑔 ∈ V |
38 |
|
difexg |
⊢ ( 𝑔 ∈ V → ( 𝑔 ∖ 𝑓 ) ∈ V ) |
39 |
37 38
|
mp1i |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∖ 𝑓 ) ∈ V ) |
40 |
|
dmexg |
⊢ ( ( 𝑔 ∖ 𝑓 ) ∈ V → dom ( 𝑔 ∖ 𝑓 ) ∈ V ) |
41 |
|
uniexg |
⊢ ( dom ( 𝑔 ∖ 𝑓 ) ∈ V → ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V ) |
42 |
39 40 41
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V ) |
43 |
42
|
ralrimivw |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑔 ∈ 𝑋 ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V ) |
44 |
|
eqid |
⊢ ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) = ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) |
45 |
44
|
fnmpt |
⊢ ( ∀ 𝑔 ∈ 𝑋 ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V → ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) Fn 𝑋 ) |
46 |
43 45
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) Fn 𝑋 ) |
47 |
|
dffn4 |
⊢ ( ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) Fn 𝑋 ↔ ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) : 𝑋 –onto→ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
48 |
46 47
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) : 𝑋 –onto→ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
49 |
|
fonum |
⊢ ( ( 𝑋 ∈ dom card ∧ ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) : 𝑋 –onto→ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) → ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ∈ dom card ) |
50 |
27 48 49
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ∈ dom card ) |
51 |
|
ssdif0 |
⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ↔ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ ) |
52 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) |
53 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ 𝑋 ) |
54 |
53 25
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ) |
55 |
|
vex |
⊢ 𝑓 ∈ V |
56 |
55
|
elixp |
⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
57 |
56
|
simprbi |
⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
58 |
54 57
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
59 |
58
|
r19.21bi |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
60 |
59
|
snssd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → { ( 𝑓 ‘ 𝑘 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) |
61 |
60
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → { ( 𝑓 ‘ 𝑘 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) |
62 |
52 61
|
eqssd |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → ∪ ( 𝐹 ‘ 𝑘 ) = { ( 𝑓 ‘ 𝑘 ) } ) |
63 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑘 ) ∈ V |
64 |
63
|
ensn1 |
⊢ { ( 𝑓 ‘ 𝑘 ) } ≈ 1o |
65 |
62 64
|
eqbrtrdi |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) |
66 |
65
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) ) |
67 |
51 66
|
syl5bir |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) ) |
68 |
67
|
con3d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o → ¬ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ ) ) |
69 |
|
neq0 |
⊢ ( ¬ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) |
70 |
68 69
|
syl6ib |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o → ∃ 𝑥 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ) |
71 |
|
eldifi |
⊢ ( 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
72 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
73 |
|
iftrue |
⊢ ( 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) = 𝑥 ) |
74 |
73 23
|
eleq12d |
⊢ ( 𝑛 = 𝑘 → ( if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
75 |
72 74
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) ) |
76 |
53 2
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ) |
77 |
55
|
elixp |
⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) ) |
78 |
77
|
simprbi |
⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) |
79 |
76 78
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) |
80 |
79
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) |
81 |
80
|
r19.21bi |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) |
82 |
|
iffalse |
⊢ ( ¬ 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) = ( 𝑓 ‘ 𝑛 ) ) |
83 |
82
|
eleq1d |
⊢ ( ¬ 𝑛 = 𝑘 → ( if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) ) |
84 |
81 83
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( ¬ 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) ) |
85 |
75 84
|
pm2.61d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) |
86 |
85
|
ralrimiva |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) |
87 |
3
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → 𝐴 ∈ 𝑉 ) |
88 |
|
mptelixpg |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) ) |
89 |
87 88
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) ) |
90 |
86 89
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ) |
91 |
90 2
|
eleqtrrdi |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ 𝑋 ) |
92 |
71 91
|
sylan2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ 𝑋 ) |
93 |
|
vex |
⊢ 𝑘 ∈ V |
94 |
93
|
unisn |
⊢ ∪ { 𝑘 } = 𝑘 |
95 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → 𝑘 ∈ 𝐴 ) |
96 |
|
eleq1w |
⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) ) |
97 |
95 96
|
syl5ibrcom |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑚 = 𝑘 → 𝑚 ∈ 𝐴 ) ) |
98 |
97
|
pm4.71rd |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑚 = 𝑘 ↔ ( 𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘 ) ) ) |
99 |
|
equequ1 |
⊢ ( 𝑛 = 𝑚 → ( 𝑛 = 𝑘 ↔ 𝑚 = 𝑘 ) ) |
100 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑚 ) ) |
101 |
99 100
|
ifbieq2d |
⊢ ( 𝑛 = 𝑚 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) = if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ) |
102 |
|
eqid |
⊢ ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) |
103 |
|
vex |
⊢ 𝑥 ∈ V |
104 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑚 ) ∈ V |
105 |
103 104
|
ifex |
⊢ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ∈ V |
106 |
101 102 105
|
fvmpt |
⊢ ( 𝑚 ∈ 𝐴 → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ) |
107 |
106
|
neeq1d |
⊢ ( 𝑚 ∈ 𝐴 → ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ) ) |
108 |
107
|
adantl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ) ) |
109 |
|
iffalse |
⊢ ( ¬ 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) = ( 𝑓 ‘ 𝑚 ) ) |
110 |
109
|
necon1ai |
⊢ ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) → 𝑚 = 𝑘 ) |
111 |
|
eldifsni |
⊢ ( 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → 𝑥 ≠ ( 𝑓 ‘ 𝑘 ) ) |
112 |
111
|
ad2antlr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑥 ≠ ( 𝑓 ‘ 𝑘 ) ) |
113 |
|
iftrue |
⊢ ( 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) = 𝑥 ) |
114 |
|
fveq2 |
⊢ ( 𝑚 = 𝑘 → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑘 ) ) |
115 |
113 114
|
neeq12d |
⊢ ( 𝑚 = 𝑘 → ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ 𝑥 ≠ ( 𝑓 ‘ 𝑘 ) ) ) |
116 |
112 115
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ) ) |
117 |
110 116
|
impbid2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ 𝑚 = 𝑘 ) ) |
118 |
108 117
|
bitrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ 𝑚 = 𝑘 ) ) |
119 |
118
|
pm5.32da |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) ↔ ( 𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘 ) ) ) |
120 |
98 119
|
bitr4d |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑚 = 𝑘 ↔ ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) ) ) |
121 |
120
|
abbidv |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → { 𝑚 ∣ 𝑚 = 𝑘 } = { 𝑚 ∣ ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) } ) |
122 |
|
df-sn |
⊢ { 𝑘 } = { 𝑚 ∣ 𝑚 = 𝑘 } |
123 |
|
df-rab |
⊢ { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } = { 𝑚 ∣ ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) } |
124 |
121 122 123
|
3eqtr4g |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → { 𝑘 } = { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } ) |
125 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑛 ) ∈ V |
126 |
103 125
|
ifex |
⊢ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ V |
127 |
126
|
rgenw |
⊢ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ V |
128 |
102
|
fnmpt |
⊢ ( ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ V → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) Fn 𝐴 ) |
129 |
127 128
|
mp1i |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) Fn 𝐴 ) |
130 |
|
ixpfn |
⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) → 𝑓 Fn 𝐴 ) |
131 |
76 130
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 Fn 𝐴 ) |
132 |
131
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → 𝑓 Fn 𝐴 ) |
133 |
|
fndmdif |
⊢ ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) → dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) = { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } ) |
134 |
129 132 133
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) = { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } ) |
135 |
124 134
|
eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → { 𝑘 } = dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) |
136 |
135
|
unieqd |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ∪ { 𝑘 } = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) |
137 |
94 136
|
eqtr3id |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → 𝑘 = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) |
138 |
|
difeq1 |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) → ( 𝑔 ∖ 𝑓 ) = ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) |
139 |
138
|
dmeqd |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) → dom ( 𝑔 ∖ 𝑓 ) = dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) |
140 |
139
|
unieqd |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) → ∪ dom ( 𝑔 ∖ 𝑓 ) = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) |
141 |
140
|
rspceeqv |
⊢ ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ 𝑋 ∧ 𝑘 = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) |
142 |
92 137 141
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) |
143 |
142
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
144 |
143
|
exlimdv |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ∃ 𝑥 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
145 |
70 144
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
146 |
145
|
expimpd |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐴 ∧ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
147 |
23
|
breq1d |
⊢ ( 𝑛 = 𝑘 → ( ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o ↔ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) ) |
148 |
147
|
notbid |
⊢ ( 𝑛 = 𝑘 → ( ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o ↔ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) ) |
149 |
148
|
elrab |
⊢ ( 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) ) |
150 |
44
|
elrnmpt |
⊢ ( 𝑘 ∈ V → ( 𝑘 ∈ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ↔ ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
151 |
150
|
elv |
⊢ ( 𝑘 ∈ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ↔ ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) |
152 |
146 149 151
|
3imtr4g |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } → 𝑘 ∈ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) ) |
153 |
152
|
ssrdv |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) |
154 |
|
ssnum |
⊢ ( ( ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ∈ dom card ∧ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ dom card ) |
155 |
50 153 154
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ dom card ) |
156 |
|
xpnum |
⊢ ( ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ∧ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ dom card ) → ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ dom card ) |
157 |
36 155 156
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ dom card ) |
158 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 ) |
159 |
|
rabexg |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V ) |
160 |
158 159
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V ) |
161 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑘 ) ∈ V |
162 |
161
|
uniex |
⊢ ∪ ( 𝐹 ‘ 𝑘 ) ∈ V |
163 |
162
|
rgenw |
⊢ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V |
164 |
|
iunexg |
⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V ) |
165 |
160 163 164
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V ) |
166 |
|
resixp |
⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ 𝐴 ∧ 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑓 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ) |
167 |
29 54 166
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑓 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ) |
168 |
167
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ ) |
169 |
|
ixpiunwdom |
⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V ∧ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V ∧ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) |
170 |
160 165 168 169
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) |
171 |
|
numwdom |
⊢ ( ( ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ dom card ∧ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ) |
172 |
157 170 171
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ) |
173 |
21 172
|
exlimddv |
⊢ ( 𝜑 → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ) |