Step |
Hyp |
Ref |
Expression |
1 |
|
fpwwe2.1 |
⊢ 𝑊 = { 〈 𝑥 , 𝑟 〉 ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } |
2 |
|
fpwwe2.2 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
3 |
|
fpwwe2.3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) |
4 |
|
fpwwe2lem9.4 |
⊢ ( 𝜑 → 𝑋 𝑊 𝑅 ) |
5 |
|
fpwwe2lem9.6 |
⊢ ( 𝜑 → 𝑌 𝑊 𝑆 ) |
6 |
|
eqid |
⊢ OrdIso ( 𝑅 , 𝑋 ) = OrdIso ( 𝑅 , 𝑋 ) |
7 |
6
|
oicl |
⊢ Ord dom OrdIso ( 𝑅 , 𝑋 ) |
8 |
|
eqid |
⊢ OrdIso ( 𝑆 , 𝑌 ) = OrdIso ( 𝑆 , 𝑌 ) |
9 |
8
|
oicl |
⊢ Ord dom OrdIso ( 𝑆 , 𝑌 ) |
10 |
|
ordtri2or2 |
⊢ ( ( Ord dom OrdIso ( 𝑅 , 𝑋 ) ∧ Ord dom OrdIso ( 𝑆 , 𝑌 ) ) → ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ∨ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) ) |
11 |
7 9 10
|
mp2an |
⊢ ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ∨ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) |
12 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → 𝐴 ∈ 𝑉 ) |
13 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) |
14 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → 𝑋 𝑊 𝑅 ) |
15 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → 𝑌 𝑊 𝑆 ) |
16 |
|
simpr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) |
17 |
1 12 13 14 15 6 8 16
|
fpwwe2lem8 |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ) |
18 |
17
|
ex |
⊢ ( 𝜑 → ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) → ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ) ) |
19 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → 𝐴 ∈ 𝑉 ) |
20 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) |
21 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → 𝑌 𝑊 𝑆 ) |
22 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → 𝑋 𝑊 𝑅 ) |
23 |
|
simpr |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) |
24 |
1 19 20 21 22 8 6 23
|
fpwwe2lem8 |
⊢ ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → ( 𝑌 ⊆ 𝑋 ∧ 𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) |
25 |
24
|
ex |
⊢ ( 𝜑 → ( dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) → ( 𝑌 ⊆ 𝑋 ∧ 𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) ) |
26 |
18 25
|
orim12d |
⊢ ( 𝜑 → ( ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ∨ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → ( ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌 ⊆ 𝑋 ∧ 𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) ) ) |
27 |
11 26
|
mpi |
⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌 ⊆ 𝑋 ∧ 𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) ) |