Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) → Fun 𝑓 ) |
2 |
1
|
anim1i |
⊢ ( ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ) |
3 |
2
|
ralimi |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ) |
4 |
|
fununi |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ∪ 𝐴 ) |
5 |
3 4
|
syl |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ∪ 𝐴 ) |
6 |
|
simpr |
⊢ ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) → Fun ◡ 𝑓 ) |
7 |
6
|
anim1i |
⊢ ( ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ) |
8 |
7
|
ralimi |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) ) |
9 |
|
funcnvuni |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( Fun ◡ 𝑓 ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ◡ ∪ 𝐴 ) |
10 |
8 9
|
syl |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → Fun ◡ ∪ 𝐴 ) |
11 |
5 10
|
jca |
⊢ ( ∀ 𝑓 ∈ 𝐴 ( ( Fun 𝑓 ∧ Fun ◡ 𝑓 ) ∧ ∀ 𝑔 ∈ 𝐴 ( 𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓 ) ) → ( Fun ∪ 𝐴 ∧ Fun ◡ ∪ 𝐴 ) ) |