Metamath Proof Explorer

Theorem ofoaf

Description: Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoaf ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ) → ( ∘f +o ↾ ( ( 𝐸 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) : ( ( 𝐸 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ⟶ ( 𝐸 ↑m 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → 𝐸 = ( ω ↑o 𝐷 ) )
2 omelon ⊢ ω ∈ On
3 simpl ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → 𝐷 ∈ On )
4 oecl ⊢ ( ( ω ∈ On ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) ∈ On )
5 2 3 4 sylancr ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ( ω ↑o 𝐷 ) ∈ On )
6 1 5 eqeltrd ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → 𝐸 ∈ On )
7 3 2 jctil ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ( ω ∈ On ∧ 𝐷 ∈ On ) )
8 peano1 ⊢ ∅ ∈ ω
9 oen0 ⊢ ( ( ( ω ∈ On ∧ 𝐷 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐷 ) )
10 7 8 9 sylancl ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ∅ ∈ ( ω ↑o 𝐷 ) )
11 10 1 eleqtrrd ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ∅ ∈ 𝐸 )
12 oveq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 +o 𝐸 ) = ( ∅ +o 𝐸 ) )
13 12 sseq2d ⊢ ( 𝑥 = ∅ → ( 𝐸 ⊆ ( 𝑥 +o 𝐸 ) ↔ 𝐸 ⊆ ( ∅ +o 𝐸 ) ) )
14 13 adantl ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 = ∅ ) → ( 𝐸 ⊆ ( 𝑥 +o 𝐸 ) ↔ 𝐸 ⊆ ( ∅ +o 𝐸 ) ) )
15 oa0r ⊢ ( 𝐸 ∈ On → ( ∅ +o 𝐸 ) = 𝐸 )
16 6 15 syl ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ( ∅ +o 𝐸 ) = 𝐸 )
17 ssid ⊢ ( ∅ +o 𝐸 ) ⊆ ( ∅ +o 𝐸 )
18 16 17 eqsstrrdi ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → 𝐸 ⊆ ( ∅ +o 𝐸 ) )
19 11 14 18 rspcedvd ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ∃ 𝑥 ∈ 𝐸 𝐸 ⊆ ( 𝑥 +o 𝐸 ) )
20 ssiun ⊢ ( ∃ 𝑥 ∈ 𝐸 𝐸 ⊆ ( 𝑥 +o 𝐸 ) → 𝐸 ⊆ ∪ 𝑥 ∈ 𝐸 ( 𝑥 +o 𝐸 ) )
21 19 20 syl ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → 𝐸 ⊆ ∪ 𝑥 ∈ 𝐸 ( 𝑥 +o 𝐸 ) )
22 1 eleq2d ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ( 𝑥 ∈ 𝐸 ↔ 𝑥 ∈ ( ω ↑o 𝐷 ) ) )
23 22 biimpa ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝑥 ∈ ( ω ↑o 𝐷 ) )
24 6 adantr ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝐸 ∈ On )
25 1 adantr ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 ∈ 𝐸 ) → 𝐸 = ( ω ↑o 𝐷 ) )
26 ssid ⊢ 𝐸 ⊆ 𝐸
27 25 26 eqsstrrdi ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 ∈ 𝐸 ) → ( ω ↑o 𝐷 ) ⊆ 𝐸 )
28 oaabs2 ⊢ ( ( ( 𝑥 ∈ ( ω ↑o 𝐷 ) ∧ 𝐸 ∈ On ) ∧ ( ω ↑o 𝐷 ) ⊆ 𝐸 ) → ( 𝑥 +o 𝐸 ) = 𝐸 )
29 23 24 27 28 syl21anc ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 ∈ 𝐸 ) → ( 𝑥 +o 𝐸 ) = 𝐸 )
30 29 26 eqsstrdi ⊢ ( ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ∧ 𝑥 ∈ 𝐸 ) → ( 𝑥 +o 𝐸 ) ⊆ 𝐸 )
31 30 iunssd ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ∪ 𝑥 ∈ 𝐸 ( 𝑥 +o 𝐸 ) ⊆ 𝐸 )
32 21 31 eqssd ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → 𝐸 = ∪ 𝑥 ∈ 𝐸 ( 𝑥 +o 𝐸 ) )
33 6 6 32 3jca ⊢ ( ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) → ( 𝐸 ∈ On ∧ 𝐸 ∈ On ∧ 𝐸 = ∪ 𝑥 ∈ 𝐸 ( 𝑥 +o 𝐸 ) ) )
34 ofoafg ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐸 ∈ On ∧ 𝐸 ∈ On ∧ 𝐸 = ∪ 𝑥 ∈ 𝐸 ( 𝑥 +o 𝐸 ) ) ) → ( ∘f +o ↾ ( ( 𝐸 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) : ( ( 𝐸 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ⟶ ( 𝐸 ↑m 𝐶 ) )
35 33 34 sylan2 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐷 ∈ On ∧ 𝐸 = ( ω ↑o 𝐷 ) ) ) → ( ∘f +o ↾ ( ( 𝐸 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ) : ( ( 𝐸 ↑m 𝐴 ) × ( 𝐸 ↑m 𝐵 ) ) ⟶ ( 𝐸 ↑m 𝐶 ) )