| Step | Hyp | Ref | Expression | 
						
							| 1 |  | dmwf | ⊢ ( 𝑅  ∈  ∪  ( 𝑅1  “  On )  →  dom  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) | 
						
							| 2 |  | rnwf | ⊢ ( 𝑅  ∈  ∪  ( 𝑅1  “  On )  →  ran  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) | 
						
							| 3 | 1 2 | jca | ⊢ ( 𝑅  ∈  ∪  ( 𝑅1  “  On )  →  ( dom  𝑅  ∈  ∪  ( 𝑅1  “  On )  ∧  ran  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) ) | 
						
							| 4 |  | xpwf | ⊢ ( ( dom  𝑅  ∈  ∪  ( 𝑅1  “  On )  ∧  ran  𝑅  ∈  ∪  ( 𝑅1  “  On ) )  →  ( dom  𝑅  ×  ran  𝑅 )  ∈  ∪  ( 𝑅1  “  On ) ) | 
						
							| 5 |  | relssdmrn | ⊢ ( Rel  𝑅  →  𝑅  ⊆  ( dom  𝑅  ×  ran  𝑅 ) ) | 
						
							| 6 |  | sswf | ⊢ ( ( ( dom  𝑅  ×  ran  𝑅 )  ∈  ∪  ( 𝑅1  “  On )  ∧  𝑅  ⊆  ( dom  𝑅  ×  ran  𝑅 ) )  →  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) | 
						
							| 7 | 5 6 | sylan2 | ⊢ ( ( ( dom  𝑅  ×  ran  𝑅 )  ∈  ∪  ( 𝑅1  “  On )  ∧  Rel  𝑅 )  →  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) | 
						
							| 8 | 7 | expcom | ⊢ ( Rel  𝑅  →  ( ( dom  𝑅  ×  ran  𝑅 )  ∈  ∪  ( 𝑅1  “  On )  →  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) ) | 
						
							| 9 | 4 8 | syl5 | ⊢ ( Rel  𝑅  →  ( ( dom  𝑅  ∈  ∪  ( 𝑅1  “  On )  ∧  ran  𝑅  ∈  ∪  ( 𝑅1  “  On ) )  →  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) ) | 
						
							| 10 | 3 9 | impbid2 | ⊢ ( Rel  𝑅  →  ( 𝑅  ∈  ∪  ( 𝑅1  “  On )  ↔  ( dom  𝑅  ∈  ∪  ( 𝑅1  “  On )  ∧  ran  𝑅  ∈  ∪  ( 𝑅1  “  On ) ) ) ) |